src/HOL/Tools/inductive_realizer.ML

--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -53,8 +53,8 @@
       | _ => vs)) (Term.add_vars prop []) [];
 
 val attach_typeS = map_types (map_atyps
-  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
-    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+  (fn TFree (s, []) => TFree (s, @{sort type})
+    | TVar (ixn, []) => TVar (ixn, @{sort type})
     | T => T));
 
 fun dt_of_intrs thy vs nparms intrs =