--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 18:19:57 2014 +0100
@@ -920,7 +920,7 @@
val Type ("fun", [T, T']) = fastype_of comb;
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
- val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
+ val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
val x = Free ("x", T)
val f = Free ("f", T' --> U)
fun apply_f f' =
@@ -947,8 +947,8 @@
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
- val T' = TFree (tname', HOLogic.typeS)
- val U = TFree (uname, HOLogic.typeS)
+ val T' = TFree (tname', @{sort type})
+ val U = TFree (uname, @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
val th' = Thm.certify_instantiate