Fix a Moscow ML compilation error from recent changes

HOL-Theorem-Prover · Jan 23, 2025 · 6c4ef89 · 6c4ef89
1 parent 8f3db54
commit 6c4ef89
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/portableML/rawtheory/RawTheoryReader.sml b/src/portableML/rawtheory/RawTheoryReader.sml
@@ -94,9 +94,9 @@ fun raw_term_decode s =
     decoding raw theorems
    ---------------------------------------------------------------------- *)
 
-fun decclass 0 = DB_dtype.Axm
-  | decclass 1 = DB_dtype.Def
-  | decclass 2 = DB_dtype.Thm
+fun decclass 0 = Axm
+  | decclass 1 = Def
+  | decclass 2 = Thm
   | decclass i = raise TheoryReader ("Bad theorem class: "^Int.toString i)
 
 val dep_decode : int raw_dep decoder = let