src/Pure/Isar/isar_syn.ML
changeset 24624 b8383b1bbae3
parent 24589 d3fca349736c
child 24748 ee0a0eb6b738
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 18 07:36:14 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 18 07:36:15 2007 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
     1.5             >> Class.interpretation_in_class_cmd
     1.6        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
     1.7 -           >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false)))
     1.8 +           >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func))
     1.9      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.10  
    1.11  val instantiationP =