# HG changeset patch # User wenzelm # Date 1425249341 -3600 # Node ID d09cc83cdce9d23a37609e333edff4205e5ef2d4 # Parent 7e4bf0824cd363efe7aee7748d16359c61dc5890 added Proof_Context.cterm_of/ctyp_of convenience; diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/expression.ML --- 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; diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/generic_target.ML --- 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; diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/local_defs.ML --- 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 diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/obtain.ML --- 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); diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/proof.ML --- 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 (); diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/proof_context.ML --- 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; diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/Isar/spec_rules.ML --- 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 => diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/ML/ml_antiquotations.ML --- 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 *) diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/simplifier.ML --- 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 diff -r 7e4bf0824cd3 -r d09cc83cdce9 src/Pure/subgoal.ML --- 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;