src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 56259 0d301d91444b
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -920,7 +920,7 @@
     1.4      val Type ("fun", [T, T']) = fastype_of comb;
     1.5      val (Const (case_name, _), fs) = strip_comb comb
     1.6      val used = Term.add_tfree_names comb []
     1.7 -    val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
     1.8 +    val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
     1.9      val x = Free ("x", T)
    1.10      val f = Free ("f", T' --> U)
    1.11      fun apply_f f' =
    1.12 @@ -947,8 +947,8 @@
    1.13      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
    1.14      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
    1.15      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
    1.16 -    val T' = TFree (tname', HOLogic.typeS)
    1.17 -    val U = TFree (uname, HOLogic.typeS)
    1.18 +    val T' = TFree (tname', @{sort type})
    1.19 +    val U = TFree (uname, @{sort type})
    1.20      val y = Free (yname, U)
    1.21      val f' = absdummy (U --> T') (Bound 0 $ y)
    1.22      val th' = Thm.certify_instantiate