src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 60805 4cc49ead6e75
parent 60696 8304fb4fb823
child 61268 abe08fb15a12
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 27 22:08:46 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Jul 27 23:40:39 2015 +0200
     1.3 @@ -947,9 +947,11 @@
     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 ctxt'
     1.8 -      ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
     1.9 -       [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    1.10 +    val th' =
    1.11 +      Thm.instantiate
    1.12 +        ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
    1.13 +          (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
    1.14 +         [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
    1.15      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
    1.16    in
    1.17      th'
    1.18 @@ -1075,10 +1077,10 @@
    1.19              val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    1.20                handle Type.TYPE_MATCH =>
    1.21                  error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
    1.22 -                  " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^
    1.23 -                  " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^
    1.24 -                  " in " ^ Display.string_of_thm ctxt th)
    1.25 -          in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
    1.26 +                  " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
    1.27 +                  " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
    1.28 +                  " in " ^ Display.string_of_thm ctxt' th)
    1.29 +          in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
    1.30          fun instantiate_typ th =
    1.31            let
    1.32              val (pred', _) = strip_intro_concl th
    1.33 @@ -1086,13 +1088,13 @@
    1.34                if not (fst (dest_Const pred) = fst (dest_Const pred')) then
    1.35                  raise Fail "Trying to instantiate another predicate"
    1.36                else ()
    1.37 -          in Thm.certify_instantiate ctxt' (subst_of (pred', pred), []) th end
    1.38 +          in Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt')) (subst_of (pred', pred)), []) th end
    1.39          fun instantiate_ho_args th =
    1.40            let
    1.41              val (_, args') =
    1.42                (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
    1.43              val ho_args' = map dest_Var (ho_args_of_typ T args')
    1.44 -          in Thm.certify_instantiate ctxt' ([], ho_args' ~~ ho_args) th end
    1.45 +          in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
    1.46          val outp_pred =
    1.47            Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    1.48          val ((_, ths'), ctxt1) =