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/Tools/class_package.ML
changeset 21359 072e83a0b5bb
parent 21094 7e18c11e6267
child 21444 8f71e2b3fd92 
--- a/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:50 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Nov 14 15:29:52 2006 +0100
@@ -208,8 +208,8 @@
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i PureThy.internalK NONE after_qed' NONE ("", [])
-      ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts)
+    |> Proof.theorem_i PureThy.internalK NONE after_qed'
+      ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
   end;
 
 in
isabelle