# HG changeset patch # User wenzelm # Date 1425659540 -3600 # Node ID 920889b0788e03a3eb7d50dd83a6e986e77cbc5f # Parent deae170e24a61454d6387fd1f38eb5449d1e5092 clarified context; diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/Isar/element.ML Fri Mar 06 17:32:20 2015 +0100 @@ -339,7 +339,7 @@ fun instantiate_tfrees thy subst th = let val idx = Thm.maxidx_of th + 1; - fun cert_inst (a, (S, T)) = (Thm.global_ctyp_of thy (TVar ((a, idx), S)), Thm.global_ctyp_of thy T); + fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T); fun add_inst (a, S) insts = if AList.defined (op =) insts a then insts diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/Isar/expression.ML Fri Mar 06 17:32:20 2015 +0100 @@ -630,7 +630,8 @@ in if bodyT = propT then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t)) - else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t)) + else + (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t)) end; (* achieve plain syntax for locale predicates (without "PROP") *) @@ -684,11 +685,11 @@ compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, - Conjunction.intr_balanced (map (Thm.assume o Thm.global_cterm_of defs_thy) norm_ts), 0) 1); + Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF - [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.global_cterm_of defs_thy statement))]) + [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt @@ -705,7 +706,7 @@ fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy = let val ctxt = Proof_Context.init_global thy; - val defs' = map (Thm.global_cterm_of thy #> Assumption.assume ctxt #> Drule.abs_def) defs; + val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs; val (a_pred, a_intro, a_axioms, thy'') = if null exts then (NONE, NONE, [], thy) @@ -806,7 +807,7 @@ val notes = if is_some asm then [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []), - [([Assumption.assume pred_ctxt (Thm.global_cterm_of thy' (the asm))], + [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))], [(Attrib.internal o K) Locale.witness_add])])])] else []; diff -r deae170e24a6 -r 920889b0788e src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/Isar/obtain.ML Fri Mar 06 17:32:20 2015 +0100 @@ -237,20 +237,20 @@ val xs = map (apsnd norm_type o fst) vars; val ys = map (apsnd norm_type) (drop m params); val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys; - val terms = map (Drule.mk_term o Thm.global_cterm_of thy o Free) (xs @ ys'); + val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys'); val instT = fold (Term.add_tvarsT o #2) params [] - |> map (TVar #> (fn T => (Thm.global_ctyp_of thy T, Thm.global_ctyp_of thy (norm_type T)))); + |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T))); val closed_rule = rule - |> Thm.forall_intr (Thm.global_cterm_of thy (Free thesis_var)) + |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) |> Thm.instantiate (instT, []); val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; val vars' = map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~ (map snd vars @ replicate (length ys) NoSyn); - val rule'' = Thm.forall_elim (Thm.global_cterm_of thy (Logic.varify_global (Free thesis_var))) rule'; + val rule'' = Thm.forall_elim (Thm.cterm_of ctxt' (Logic.varify_global (Free thesis_var))) rule'; in ((vars', rule''), ctxt') end; fun inferred_type (binding, _, mx) ctxt = diff -r deae170e24a6 -r 920889b0788e src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 06 17:32:20 2015 +0100 @@ -116,8 +116,8 @@ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; val inst_vars = map_filter (make_inst inst2) vars2; in - (map (apply2 (Thm.global_ctyp_of thy)) inst_tvars, - map (apply2 (Thm.global_cterm_of thy)) inst_vars) + (map (apply2 (Thm.ctyp_of ctxt)) inst_tvars, + map (apply2 (Thm.cterm_of ctxt)) inst_vars) end; fun where_rule ctxt mixed_insts fixes thm = @@ -248,9 +248,7 @@ val envT' = map (fn (ixn, T) => (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; val cenv = - map - (fn (xi, t) => - apply2 (Thm.global_cterm_of thy) (Var (xi, fastype_of t), t)) + map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) (distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xis ~~ ts)); @@ -264,7 +262,7 @@ fun liftterm t = fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t); fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct); - val lifttvar = apply2 (Thm.global_ctyp_of thy o Logic.incr_tvar inc); + val lifttvar = apply2 (Thm.ctyp_of ctxt' o Logic.incr_tvar inc); val rule = Drule.instantiate_normalize (map lifttvar envT', map liftpair cenv) (Thm.lift_rule cgoal thm) @@ -281,9 +279,8 @@ fun make_elim_preserve ctxt rl = let - val thy = Thm.theory_of_thm rl; val maxidx = Thm.maxidx_of rl; - fun cvar xi = Thm.global_cterm_of thy (Var (xi, propT)); + fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)), (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl; diff -r deae170e24a6 -r 920889b0788e src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/goal.ML Fri Mar 06 17:32:20 2015 +0100 @@ -127,21 +127,19 @@ fun future_result ctxt result prop = let - val thy = Proof_Context.theory_of ctxt; - val assms = Assumption.all_assms_of ctxt; val As = map Thm.term_of assms; val xs = map Free (fold Term.add_frees (prop :: As) []); - val fixes = map (Thm.global_cterm_of thy) xs; + val fixes = map (Thm.cterm_of ctxt) xs; val tfrees = fold Term.add_tfrees (prop :: As) []; val instT = - map (fn (a, S) => (Thm.global_ctyp_of thy (TVar ((a, 0), S)), Thm.global_ctyp_of thy (TFree (a, S)))) tfrees; + map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees; val global_prop = Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))) - |> Thm.global_cterm_of thy + |> Thm.cterm_of ctxt |> Thm.weaken_sorts (Variable.sorts_of ctxt); val global_result = result |> Future.map (Drule.flexflex_unique (SOME ctxt) #> @@ -191,7 +189,7 @@ ("The error(s) above occurred for the goal statement" ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt (Logic.list_implies (asms, Logic.mk_conjunction_list props))); - fun cert_safe t = Thm.global_cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t)) + fun cert_safe t = Thm.cterm_of ctxt (Envir.beta_norm (Term.no_dummy_patterns t)) handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; val casms = map cert_safe asms; val cprops = map cert_safe props; diff -r deae170e24a6 -r 920889b0788e src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/more_thm.ML Fri Mar 06 17:32:20 2015 +0100 @@ -118,7 +118,9 @@ let val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; - in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t end; + in + Term.fold_aterms (fn v as Free _ => insert (op aconvc) (Thm.global_cterm_of thy v) | _ => I) t + end; (* cterm constructors and destructors *) @@ -349,8 +351,8 @@ (* certify_instantiate *) fun certify_inst thy (instT, inst) = - (map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT, - map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst); + (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT, + map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst); fun certify_instantiate insts th = Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th; diff -r deae170e24a6 -r 920889b0788e src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Mar 06 16:09:51 2015 +0100 +++ b/src/Pure/variable.ML Fri Mar 06 17:32:20 2015 +0100 @@ -587,9 +587,8 @@ fun focus_cterm goal ctxt = let - val thy = Thm.theory_of_cterm goal; val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt; - val ps' = map (Thm.global_cterm_of thy o Free) ps; + val ps' = map (Thm.cterm_of ctxt' o Free) ps; val goal' = fold forall_elim_prop ps' goal; in ((xs ~~ ps', goal'), ctxt') end;