src/Tools/Code/code_ml.ML
changeset 33038 8f9594c31de4
parent 32926 342d89e5a808
child 33519 e31a85f92ce9
--- a/src/Tools/Code/code_ml.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -1028,7 +1028,7 @@
     val tyco = Sign.intern_type thy raw_tyco;
     val constrs = map (Code.check_const thy) raw_constrs;
     val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
-    val _ = if gen_eq_set (op =) (constrs, constrs') then ()
+    val _ = if eq_set (op =) (constrs, constrs') then ()
       else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
     val is_first = is_first_occ background;
     val background' = register_datatype tyco constrs background;