src/Pure/global_theory.ML
changeset 68558 7aae213d9e69
parent 68540 000a0e062529
child 68661 5820f0f379ae
     1.1 --- a/src/Pure/global_theory.ML	Sun Jul 01 12:37:24 2018 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sun Jul 01 12:38:37 2018 +0200
     1.3 @@ -24,8 +24,6 @@
     1.4    val name_thm: bool -> bool -> string -> thm -> thm
     1.5    val name_thms: bool -> bool -> string -> thm list -> thm list
     1.6    val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
     1.7 -  val pending_shyps_raw: Config.raw
     1.8 -  val pending_shyps: bool Config.T
     1.9    val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
    1.10    val store_thm: binding * thm -> theory -> thm * theory
    1.11    val store_thm_open: binding * thm -> theory -> thm * theory
    1.12 @@ -130,9 +128,6 @@
    1.13  
    1.14  fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
    1.15  
    1.16 -val pending_shyps_raw = Config.declare ("pending_shyps", \<^here>) (K (Config.Bool false));
    1.17 -val pending_shyps = Config.bool pending_shyps_raw;
    1.18 -
    1.19  fun add_facts (b, fact) thy =
    1.20    let
    1.21      val full_name = Sign.full_name thy b;
    1.22 @@ -148,8 +143,6 @@
    1.23            val prop = Thm.plain_prop_of thm
    1.24              handle THM _ =>
    1.25                thm
    1.26 -              |> not (Config.get_global thy pending_shyps) ?
    1.27 -                  Thm.check_shyps (Proof_Context.init_global thy)
    1.28                |> Thm.check_hyps (Context.Theory thy)
    1.29                |> Thm.full_prop_of;
    1.30          in