--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 18:19:57 2014 +0100
@@ -36,7 +36,7 @@
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
val rec_result_Ts = map (fn ((i, _), P) =>
- if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
+ if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
(descr ~~ pnames);
fun make_pred i T U r x =
@@ -163,8 +163,8 @@
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
- val rT = TFree ("'P", HOLogic.typeS);
- val rT' = TVar (("'P", 0), HOLogic.typeS);
+ val rT = TFree ("'P", @{sort type});
+ val rT' = TVar (("'P", 0), @{sort type});
fun make_casedist_prem T (cname, cargs) =
let