1.1 --- a/src/Pure/Isar/class_target.ML	Wed Jan 21 23:40:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -55,8 +55,6 @@
     1.4      -> (Attrib.binding * string list) list
     1.5      -> theory -> class * theory
     1.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     1.7 -
     1.8 -  (*old instance layer*)
     1.9    val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    1.10    val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
    1.11  end;
    1.12 @@ -275,7 +273,7 @@
    1.13      val intros = (snd o rules thy) sup :: map_filter I
    1.14        [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    1.15          (fst o rules thy) sub];
    1.16 -    val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
    1.17 +    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
    1.18      val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.19        (K tac);
    1.20      val diff_sort = Sign.complete_sort thy [sup]
    1.21 @@ -285,9 +283,9 @@
    1.22      |> AxClass.add_classrel classrel
    1.23      |> ClassData.map (Graph.add_edge (sub, sup))
    1.24      |> activate_defs sub (these_defs thy diff_sort)
    1.25 -    |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
    1.26 -        dep_morph $> Element.satisfy_morphism [wit] $> export))
    1.27 -          (the_list some_dep_morph) (the_list some_wit)
    1.28 +    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
    1.29 +        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
    1.30 +          (the_list some_dep_morph)
    1.31      |> (fn thy => fold_rev Locale.activate_global_facts
    1.32        (Locale.get_registrations thy) thy)
    1.33    end;