src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 60367 e201bd8973db
parent 59636 9f44d053b972
child 60696 8304fb4fb823
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Jun 02 23:00:50 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jun 03 19:25:05 2015 +0200
     1.3 @@ -947,7 +947,7 @@
     1.4      val U = TFree ("'u", @{sort type})
     1.5      val y = Free (yname, U)
     1.6      val f' = absdummy (U --> T') (Bound 0 $ y)
     1.7 -    val th' = Thm.certify_instantiate
     1.8 +    val th' = Thm.certify_instantiate ctxt
     1.9        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    1.10         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    1.11      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
    1.12 @@ -1086,13 +1086,13 @@
    1.13                if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    1.14                  raise Fail "Trying to instantiate another predicate"
    1.15                else ()
    1.16 -          in Thm.certify_instantiate (subst_of (pred', pred), []) th end
    1.17 +          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
    1.18          fun instantiate_ho_args th =
    1.19            let
    1.20              val (_, args') =
    1.21                (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
    1.22              val ho_args' = map dest_Var (ho_args_of_typ T args')
    1.23 -          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
    1.24 +          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
    1.25          val outp_pred =
    1.26            Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    1.27          val ((_, ths'), ctxt1) =