src/Pure/pure_thy.ML
changeset 36106 19deea200358
parent 35985 0bbf0d2348f9
child 36744 6e1f3d609a68
     1.1 --- a/src/Pure/pure_thy.ML	Sun Apr 11 14:06:35 2010 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Sun Apr 11 14:30:34 2010 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4  fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
     1.5    let
     1.6      val prop = prep thy (b, raw_prop);
     1.7 -    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     1.8 +    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     1.9      val thm = def
    1.10        |> Thm.forall_intr_frees
    1.11        |> Thm.forall_elim_vars 0