src/Pure/global_theory.ML
changeset 61261 ddb2da7cb2e4
parent 61054 add998b3c597
child 61262 7bd1eb4b056e
     1.1 --- a/src/Pure/global_theory.ML	Thu Sep 24 13:33:42 2015 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Thu Sep 24 23:33:29 2015 +0200
     1.3 @@ -207,7 +207,7 @@
     1.4    let
     1.5      val ctxt = Syntax.init_pretty_global thy;
     1.6      val prop = prep ctxt (b, raw_prop);
     1.7 -    val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
     1.8 +    val ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy;
     1.9      val thm = def
    1.10        |> Thm.forall_intr_frees
    1.11        |> Thm.forall_elim_vars 0