src/Pure/Isar/isar_syn.ML
changeset 24423 ae9cd0e92423
parent 24314 665b3ab2dabe
child 24451 7c205d006719
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
     1.5             >> Class.instance_sort_cmd
     1.6        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
     1.7 -           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs)
     1.8 +           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
     1.9      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.10  
    1.11  end;
    1.12 @@ -441,7 +441,7 @@
    1.13  
    1.14  val code_datatypeP =
    1.15    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
    1.16 -    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_consts_cmd));
    1.17 +    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
    1.18  
    1.19  
    1.20