src/Pure/Isar/class.ML
changeset 25094 ba43514068fd
parent 25083 765528b4b419
child 25096 b8950f7cf92e
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 19 10:44:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 19 12:21:32 2007 +0200
     1.3 @@ -520,7 +520,8 @@
     1.4    in
     1.5      thy
     1.6      |> fold_map (get_remove_global_constraint o fst o snd) params
     1.7 -    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs)
     1.8 +    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
     1.9 +          (inst, map (fn def => (("", []), def)) defs)
    1.10      |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
    1.11    end;
    1.12