--- a/src/Pure/Isar/expression.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/expression.ML Sun Mar 01 23:35:41 2015 +0100
@@ -758,7 +758,7 @@
fun defines_to_notes ctxt (Defines defs) =
Notes ("", map (fn (a, (def, _)) =>
- (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
+ (a, [([Assumption.assume ctxt (Proof_Context.cterm_of ctxt def)],
[(Attrib.internal o K) Locale.witness_add])])) defs)
| defines_to_notes _ e = e;
--- a/src/Pure/Isar/generic_target.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/generic_target.ML Sun Mar 01 23:35:41 2015 +0100
@@ -206,8 +206,7 @@
(*result*)
val def =
Thm.transitive local_def global_def
- |> Local_Defs.contract lthy3 defs
- (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
+ |> Local_Defs.contract lthy3 defs (Proof_Context.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
val ([(res_name, [res])], lthy4) = lthy3
|> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
in ((lhs, (res_name, res)), lthy4) end;
--- a/src/Pure/Isar/local_defs.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/local_defs.ML Sun Mar 01 23:35:41 2015 +0100
@@ -214,7 +214,7 @@
fun derived_def ctxt conditional prop =
let
val ((c, T), rhs) = prop
- |> Thm.cterm_of (Proof_Context.theory_of ctxt)
+ |> Proof_Context.cterm_of ctxt
|> meta_rewrite_conv ctxt
|> (snd o Logic.dest_equals o Thm.prop_of)
|> conditional ? Logic.strip_imp_concl
--- a/src/Pure/Isar/obtain.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Mar 01 23:35:41 2015 +0100
@@ -187,8 +187,7 @@
fun result tac facts ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
+ val cert = Proof_Context.cterm_of ctxt;
val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
val rule =
@@ -270,9 +269,8 @@
fun gen_guess prep_vars raw_vars int state =
let
val _ = Proof.assert_forward_or_chain state;
- val thy = Proof.theory_of state;
- val cert = Thm.cterm_of thy;
val ctxt = Proof.context_of state;
+ val cert = Proof_Context.cterm_of ctxt;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
--- a/src/Pure/Isar/proof.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/proof.ML Sun Mar 01 23:35:41 2015 +0100
@@ -892,8 +892,8 @@
fun generic_goal prepp kind before_qed after_qed raw_propp state =
let
- val thy = theory_of state;
- val cert = Thm.cterm_of thy;
+ val ctxt = context_of state;
+ val cert = Proof_Context.cterm_of ctxt;
val chaining = can assert_chain state;
val pos = Position.thread_data ();
--- a/src/Pure/Isar/proof_context.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 01 23:35:41 2015 +0100
@@ -11,6 +11,8 @@
val theory_of: Proof.context -> theory
val init_global: theory -> Proof.context
val get_global: theory -> string -> Proof.context
+ val cterm_of: Proof.context -> term -> cterm
+ val ctyp_of: Proof.context -> typ -> ctyp
type mode
val mode_default: mode
val mode_stmt: mode
@@ -180,6 +182,9 @@
val init_global = Proof_Context.init_global;
val get_global = Proof_Context.get_global;
+val cterm_of = Thm.cterm_of o theory_of;
+val ctyp_of = Thm.ctyp_of o theory_of;
+
(** inner syntax mode **)
@@ -1161,7 +1166,7 @@
fun gen_assms prepp exp args ctxt =
let
- val cert = Thm.cterm_of (theory_of ctxt);
+ val cert = cterm_of ctxt;
val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
val _ = Variable.warn_extra_tfrees ctxt ctxt1;
val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
--- a/src/Pure/Isar/spec_rules.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/Isar/spec_rules.ML Sun Mar 01 23:35:41 2015 +0100
@@ -48,7 +48,7 @@
fun add class (ts, ths) lthy =
let
- val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
+ val cts = map (Proof_Context.cterm_of lthy) ts;
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi =>
--- a/src/Pure/ML/ml_antiquotations.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sun Mar 01 23:35:41 2015 +0100
@@ -62,22 +62,18 @@
ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
- "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
+ "Proof_Context.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+ "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+ "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
ML_Antiquotation.value @{binding cpat}
(Args.context --
Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
- "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t))));
+ "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
(* type classes *)
--- a/src/Pure/simplifier.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/simplifier.ML Sun Mar 01 23:35:41 2015 +0100
@@ -132,8 +132,7 @@
let
val lhss' = prep lthy lhss;
val ctxt' = fold Variable.auto_fixes lhss' lthy;
- in Variable.export_terms ctxt' lthy lhss' end
- |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
+ in Variable.export_terms ctxt' lthy lhss' end |> map (Proof_Context.cterm_of lthy),
proc = proc,
identifier = identifier};
in
--- a/src/Pure/subgoal.ML Sun Mar 01 14:15:49 2015 +0100
+++ b/src/Pure/subgoal.ML Sun Mar 01 23:35:41 2015 +0100
@@ -67,7 +67,7 @@
*)
fun lift_import idx params th ctxt =
let
- val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
+ val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
val Ts = map (#T o Thm.rep_cterm) params;