Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/pure_thy.ML
changeset 36106 19deea200358
parent 35985 0bbf0d2348f9
child 36744 6e1f3d609a68 
--- a/src/Pure/pure_thy.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/pure_thy.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -210,7 +210,7 @@
 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   let
     val prop = prep thy (b, raw_prop);
-    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees
       |> Thm.forall_elim_vars 0
isabelle