src/Pure/Isar/class.ML
changeset 35120 0a3adceb9c67
parent 35021 c839a4c670c6
child 35669 a91c7ed801b8
     1.1 --- a/src/Pure/Isar/class.ML	Thu Feb 11 23:50:38 2010 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Feb 12 09:49:28 2010 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Pure/Isar/ML
     1.5 +(*  Title:      Pure/Isar/class.ML
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  
     1.8  Type classes derived from primitive axclasses and locales - interfaces.
     1.9 @@ -132,7 +132,7 @@
    1.10        (Syntax.add_typ_check level name (fn xs => fn ctxt =>
    1.11          let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
    1.12  
    1.13 -    (* preprocessing elements, retrieving base sort from typechecked elements *)
    1.14 +    (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.15      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.16        #> redeclare_operations thy sups
    1.17        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc