src/Pure/Isar/proof_context.ML
changeset 59621 291934bac95e
parent 59616 eb59c6968219
child 59795 d453c69596cc
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -11,8 +11,6 @@
     1.4    val theory_of: Proof.context -> theory
     1.5    val init_global: theory -> Proof.context
     1.6    val get_global: theory -> string -> Proof.context
     1.7 -  val cterm_of: Proof.context -> term -> cterm
     1.8 -  val ctyp_of: Proof.context -> typ -> ctyp
     1.9    type mode
    1.10    val mode_default: mode
    1.11    val mode_stmt: mode
    1.12 @@ -182,9 +180,6 @@
    1.13  val init_global = Proof_Context.init_global;
    1.14  val get_global = Proof_Context.get_global;
    1.15  
    1.16 -val cterm_of = Thm.cterm_of o theory_of;
    1.17 -val ctyp_of = Thm.ctyp_of o theory_of;
    1.18 -
    1.19  
    1.20  
    1.21  (** inner syntax mode **)
    1.22 @@ -1169,7 +1164,7 @@
    1.23      val ((propss, _), ctxt1) = prepp (map snd args) ctxt;
    1.24      val _ = Variable.warn_extra_tfrees ctxt ctxt1;
    1.25      val (premss, ctxt2) =
    1.26 -      fold_burrow (Assumption.add_assms exp o map (cterm_of ctxt)) propss ctxt1;
    1.27 +      fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss ctxt1;
    1.28    in
    1.29      ctxt2
    1.30      |> auto_bind_facts (flat propss)