thy_decl outer syntax for repdef
authorhuffman
Thu, 19 Nov 2009 23:15:24 -0800
changeset 33812 10c335383c8b
parent 33811 b1b66441275d
child 33813 0bc8d4f786bd
thy_decl outer syntax for repdef
src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Thu Nov 19 22:30:14 2009 -0800
+++ b/src/HOLCF/Tools/repdef.ML	Thu Nov 19 23:15:24 2009 -0800
@@ -172,7 +172,7 @@
     ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
 
 val _ =
-  OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_goal
+  OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
     (repdef_decl >>
       (Toplevel.print oo (Toplevel.theory o mk_repdef)));