src/Pure/goals.ML

--- a/src/Pure/goals.ML	Mon Jun 20 22:13:58 2005 +0200
+++ b/src/Pure/goals.ML	Mon Jun 20 22:13:59 2005 +0200
@@ -315,7 +315,7 @@
 fun get_thmx f get thy name =
   (case get_first (get_thm_locale name) (get_scope thy) of
     SOME thm => f thm
-  | NONE => get thy (name, NONE));
+  | NONE => get thy (Name name));
 
 val get_thm = get_thmx I PureThy.get_thm;
 val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;