src/HOL/HOL.thy
changeset 31299 0c5baf034d0e
parent 31173 bbe9e29b9672
child 31804 627d142fce19
--- a/src/HOL/HOL.thy	Sat May 30 11:57:36 2009 +0200
+++ b/src/HOL/HOL.thy	Sat May 30 12:52:57 2009 +0200
@@ -31,7 +31,7 @@
   ("Tools/recfun_codegen.ML")
 begin
 
-setup {* Intuitionistic.method_setup "iprover" *}
+setup {* Intuitionistic.method_setup @{binding iprover} *}
 
 
 subsection {* Primitive logic *}