# HG changeset patch
# User huffman
# Date 1258701324 28800
# Node ID 10c335383c8bee4c2a390134bd6e2bf065a0777b
# Parent  b1b66441275d3ac3b1df10da13d91496f4fa1416
thy_decl outer syntax for repdef

diff -r b1b66441275d -r 10c335383c8b 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)));