src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 56259 0d301d91444b
parent 56254 a2dd9200854d
child 57962 0284a7d083be
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Mar 22 22:00:26 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sun Mar 23 15:46:21 2014 +0100
     1.3 @@ -944,17 +944,17 @@
     1.4    let
     1.5      val th = case_rewrite thy Tcon
     1.6      val ctxt = Proof_Context.init_global thy
     1.7 -    val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
     1.8 +    val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
     1.9      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
    1.10 -    val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
    1.11 -    val T' = TFree (tname', @{sort type})
    1.12 -    val U = TFree (uname, @{sort type})
    1.13 +    val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt
    1.14 +    val T' = TFree ("'t'", @{sort type})
    1.15 +    val U = TFree ("'u", @{sort type})
    1.16      val y = Free (yname, U)
    1.17      val f' = absdummy (U --> T') (Bound 0 $ y)
    1.18      val th' = Thm.certify_instantiate
    1.19        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    1.20         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    1.21 -    val [th'] = Variable.export ctxt' ctxt [th']
    1.22 +    val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
    1.23    in
    1.24      th'
    1.25    end