src/HOL/Tools/datatype_package.ML
changeset 27261 5b3101338f42
parent 27130 4ba366056426
child 27277 7b7ce2d7fafe
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Jun 18 18:55:08 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Jun 18 18:55:10 2008 +0200
     1.3 @@ -544,7 +544,7 @@
     1.4    end;
     1.5  
     1.6  val rep_datatype = gen_rep_datatype Sign.cert_term;
     1.7 -val rep_datatype_cmd = gen_rep_datatype Sign.read_term (K I);
     1.8 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
     1.9  
    1.10  
    1.11