added Proof_Context.cterm_of/ctyp_of convenience;
authorwenzelm
Sun Mar 01 23:35:41 2015 +0100 (2015-03-01)
changeset 59573d09cc83cdce9
parent 59572 7e4bf0824cd3
child 59574 de392405a851
added Proof_Context.cterm_of/ctyp_of convenience;
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/spec_rules.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/simplifier.ML
src/Pure/subgoal.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 01 14:15:49 2015 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 01 23:35:41 2015 +0100
     1.3 @@ -758,7 +758,7 @@
     1.4  
     1.5  fun defines_to_notes ctxt (Defines defs) =
     1.6        Notes ("", map (fn (a, (def, _)) =>
     1.7 -        (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
     1.8 +        (a, [([Assumption.assume ctxt (Proof_Context.cterm_of ctxt def)],
     1.9            [(Attrib.internal o K) Locale.witness_add])])) defs)
    1.10    | defines_to_notes _ e = e;
    1.11  
     2.1 --- a/src/Pure/Isar/generic_target.ML	Sun Mar 01 14:15:49 2015 +0100
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Mar 01 23:35:41 2015 +0100
     2.3 @@ -206,8 +206,7 @@
     2.4      (*result*)
     2.5      val def =
     2.6        Thm.transitive local_def global_def
     2.7 -      |> Local_Defs.contract lthy3 defs
     2.8 -          (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
     2.9 +      |> Local_Defs.contract lthy3 defs (Proof_Context.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
    2.10      val ([(res_name, [res])], lthy4) = lthy3
    2.11        |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
    2.12    in ((lhs, (res_name, res)), lthy4) end;
     3.1 --- a/src/Pure/Isar/local_defs.ML	Sun Mar 01 14:15:49 2015 +0100
     3.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Mar 01 23:35:41 2015 +0100
     3.3 @@ -214,7 +214,7 @@
     3.4  fun derived_def ctxt conditional prop =
     3.5    let
     3.6      val ((c, T), rhs) = prop
     3.7 -      |> Thm.cterm_of (Proof_Context.theory_of ctxt)
     3.8 +      |> Proof_Context.cterm_of ctxt
     3.9        |> meta_rewrite_conv ctxt
    3.10        |> (snd o Logic.dest_equals o Thm.prop_of)
    3.11        |> conditional ? Logic.strip_imp_concl
     4.1 --- a/src/Pure/Isar/obtain.ML	Sun Mar 01 14:15:49 2015 +0100
     4.2 +++ b/src/Pure/Isar/obtain.ML	Sun Mar 01 23:35:41 2015 +0100
     4.3 @@ -187,8 +187,7 @@
     4.4  
     4.5  fun result tac facts ctxt =
     4.6    let
     4.7 -    val thy = Proof_Context.theory_of ctxt;
     4.8 -    val cert = Thm.cterm_of thy;
     4.9 +    val cert = Proof_Context.cterm_of ctxt;
    4.10  
    4.11      val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
    4.12      val rule =
    4.13 @@ -270,9 +269,8 @@
    4.14  fun gen_guess prep_vars raw_vars int state =
    4.15    let
    4.16      val _ = Proof.assert_forward_or_chain state;
    4.17 -    val thy = Proof.theory_of state;
    4.18 -    val cert = Thm.cterm_of thy;
    4.19      val ctxt = Proof.context_of state;
    4.20 +    val cert = Proof_Context.cterm_of ctxt;
    4.21      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    4.22  
    4.23      val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
     5.1 --- a/src/Pure/Isar/proof.ML	Sun Mar 01 14:15:49 2015 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Sun Mar 01 23:35:41 2015 +0100
     5.3 @@ -892,8 +892,8 @@
     5.4  
     5.5  fun generic_goal prepp kind before_qed after_qed raw_propp state =
     5.6    let
     5.7 -    val thy = theory_of state;
     5.8 -    val cert = Thm.cterm_of thy;
     5.9 +    val ctxt = context_of state;
    5.10 +    val cert = Proof_Context.cterm_of ctxt;
    5.11      val chaining = can assert_chain state;
    5.12      val pos = Position.thread_data ();
    5.13  
     6.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 01 14:15:49 2015 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 01 23:35:41 2015 +0100
     6.3 @@ -11,6 +11,8 @@
     6.4    val theory_of: Proof.context -> theory
     6.5    val init_global: theory -> Proof.context
     6.6    val get_global: theory -> string -> Proof.context
     6.7 +  val cterm_of: Proof.context -> term -> cterm
     6.8 +  val ctyp_of: Proof.context -> typ -> ctyp
     6.9    type mode
    6.10    val mode_default: mode
    6.11    val mode_stmt: mode
    6.12 @@ -180,6 +182,9 @@
    6.13  val init_global = Proof_Context.init_global;
    6.14  val get_global = Proof_Context.get_global;
    6.15  
    6.16 +val cterm_of = Thm.cterm_of o theory_of;
    6.17 +val ctyp_of = Thm.ctyp_of o theory_of;
    6.18 +
    6.19  
    6.20  
    6.21  (** inner syntax mode **)
    6.22 @@ -1161,7 +1166,7 @@
    6.23  
    6.24  fun gen_assms prepp exp args ctxt =
    6.25    let
    6.26 -    val cert = Thm.cterm_of (theory_of ctxt);
    6.27 +    val cert = cterm_of ctxt;
    6.28      val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
    6.29      val _ = Variable.warn_extra_tfrees ctxt ctxt1;
    6.30      val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1;
     7.1 --- a/src/Pure/Isar/spec_rules.ML	Sun Mar 01 14:15:49 2015 +0100
     7.2 +++ b/src/Pure/Isar/spec_rules.ML	Sun Mar 01 23:35:41 2015 +0100
     7.3 @@ -48,7 +48,7 @@
     7.4  
     7.5  fun add class (ts, ths) lthy =
     7.6    let
     7.7 -    val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
     7.8 +    val cts = map (Proof_Context.cterm_of lthy) ts;
     7.9    in
    7.10      lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
    7.11        (fn phi =>
     8.1 --- a/src/Pure/ML/ml_antiquotations.ML	Sun Mar 01 14:15:49 2015 +0100
     8.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sun Mar 01 23:35:41 2015 +0100
     8.3 @@ -62,22 +62,18 @@
     8.4    ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
     8.5  
     8.6    ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
     8.7 -    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
     8.8 -      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
     8.9 +    "Proof_Context.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    8.10  
    8.11    ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
    8.12 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    8.13 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    8.14 +    "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    8.15  
    8.16    ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
    8.17 -    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    8.18 -     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    8.19 +    "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    8.20  
    8.21    ML_Antiquotation.value @{binding cpat}
    8.22      (Args.context --
    8.23        Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
    8.24 -        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    8.25 -          ML_Syntax.atomic (ML_Syntax.print_term t))));
    8.26 +        "Proof_Context.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
    8.27  
    8.28  
    8.29  (* type classes *)
     9.1 --- a/src/Pure/simplifier.ML	Sun Mar 01 14:15:49 2015 +0100
     9.2 +++ b/src/Pure/simplifier.ML	Sun Mar 01 23:35:41 2015 +0100
     9.3 @@ -132,8 +132,7 @@
     9.4          let
     9.5            val lhss' = prep lthy lhss;
     9.6            val ctxt' = fold Variable.auto_fixes lhss' lthy;
     9.7 -        in Variable.export_terms ctxt' lthy lhss' end
     9.8 -        |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
     9.9 +        in Variable.export_terms ctxt' lthy lhss' end |> map (Proof_Context.cterm_of lthy),
    9.10         proc = proc,
    9.11         identifier = identifier};
    9.12    in
    10.1 --- a/src/Pure/subgoal.ML	Sun Mar 01 14:15:49 2015 +0100
    10.2 +++ b/src/Pure/subgoal.ML	Sun Mar 01 23:35:41 2015 +0100
    10.3 @@ -67,7 +67,7 @@
    10.4  *)
    10.5  fun lift_import idx params th ctxt =
    10.6    let
    10.7 -    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
    10.8 +    val cert = Proof_Context.cterm_of ctxt;
    10.9      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
   10.10  
   10.11      val Ts = map (#T o Thm.rep_cterm) params;