# HG changeset patch
# User wenzelm
# Date 1323897004 -3600
# Node ID 061ef175f7a1add1ad4efcf2ecfe4dce4cbe1166
# Parent  71b8d0d170b1baf671448cc1e7b060260b3e0f79
tuned signature;

diff -r 71b8d0d170b1 -r 061ef175f7a1 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 21:54:32 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 14 22:10:04 2011 +0100
@@ -11,7 +11,8 @@
     thm -> thm list list -> thm list list -> theory -> string list * theory
   val rep_datatype : config -> (string list -> Proof.context -> Proof.context) ->
     term list -> theory -> Proof.state
-  val rep_datatype_cmd : string list -> theory -> Proof.state
+  val rep_datatype_cmd : config -> (string list -> Proof.context -> Proof.context) ->
+    string list -> theory -> Proof.state
   val get_info : theory -> string -> info option
   val the_info : theory -> string -> info
   val the_descr : theory -> string list ->
@@ -432,7 +433,7 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global Datatype_Aux.default_config (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global;
 
 
 
@@ -451,7 +452,8 @@
 val _ =
   Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
     (Scan.repeat1 Parse.term >> (fn ts =>
-      Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd ts)));
+      Toplevel.print o
+      Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
 
 
 open Datatype_Aux;