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/FOL/ex/LocaleTest.thy
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 26645 e114be97befe 
--- a/src/FOL/ex/LocaleTest.thy	Wed Mar 19 22:50:42 2008 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Thu Mar 20 00:20:44 2008 +0100
@@ -19,7 +19,7 @@
 ML {*
   fun check_thm name = let
     val thy = the_context ();
-    val thm = get_thm thy (Facts.Named (name, NONE));
+    val thm = PureThy.get_thm thy name;
     val {prop, hyps, ...} = rep_thm thm;
     val prems = Logic.strip_imp_prems prop;
     val _ = if null hyps then ()
isabelle