src/Pure/Isar/class.ML
changeset 28085 914183e229e9
parent 28084 a05ca48ef263
child 28110 9d121b171a0a
     1.1 --- a/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 02 17:31:20 2008 +0200
     1.3 @@ -373,7 +373,7 @@
     1.4    in
     1.5      thy
     1.6      |> fold2 add_constraint (map snd consts) no_constraints
     1.7 -    |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
     1.8 +    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
     1.9            (inst, map (fn def => (Attrib.no_binding, def)) defs)
    1.10      |> fold2 add_constraint (map snd consts) constraints
    1.11    end;