src/Pure/Isar/class.ML
changeset 41270 dea60d052923
parent 40627 becf5d5187cc
child 42359 6ca5407863ed
     1.1 --- a/src/Pure/Isar/class.ML	Sat Dec 18 14:02:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Dec 18 18:43:13 2010 +0100
     1.3 @@ -232,7 +232,7 @@
     1.4        |> filter (is_class thy);
     1.5      val add_dependency = case some_dep_morph
     1.6       of SOME dep_morph => Locale.add_dependency sub
     1.7 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
     1.8 +          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
     1.9        | NONE => I
    1.10    in
    1.11      thy