src/HOL/Tools/inductive_realizer.ML
changeset 19806 f860b7a98445
parent 19617 7cb4b67d4b97
child 20071 8f3e1ddb50e6
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -60,9 +60,9 @@
     val params = map dest_Var ts;
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
-      map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
+      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
-          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
+          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
             NoSyn);
   in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
     map constr_of_intr intrs)