1.1 --- a/src/Pure/Isar/class.ML	Wed Mar 21 23:41:22 2012 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Mar 22 10:10:30 2012 +0100
     1.3 @@ -145,10 +145,12 @@
     1.4  fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
     1.5  
     1.6  val base_morphism = #base_morph oo the_class_data;
     1.7 +
     1.8  fun morphism thy class =
     1.9    (case Element.eq_morphism thy (these_defs thy [class]) of
    1.10      SOME eq_morph => base_morphism thy class $> eq_morph
    1.11    | NONE => base_morphism thy class);
    1.12 +
    1.13  val export_morphism = #export_morph oo the_class_data;
    1.14  
    1.15  fun print_classes ctxt =
    1.16 @@ -228,9 +230,9 @@
    1.17      val intros = (snd o rules thy) sup :: map_filter I
    1.18        [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
    1.19          (fst o rules thy) sub];
    1.20 -    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
    1.21 -    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.22 -      (K tac);
    1.23 +    val classrel =
    1.24 +      Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.25 +        (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
    1.26      val diff_sort = Sign.complete_sort thy [sup]
    1.27        |> subtract (op =) (Sign.complete_sort thy [sub])
    1.28        |> filter (is_class thy);
    1.29 @@ -312,14 +314,14 @@
    1.30  
    1.31  val class_prefix = Logic.const_of_class o Long_Name.base_name;
    1.32  
    1.33 +local
    1.34 +
    1.35  fun target_extension f class lthy =
    1.36    lthy
    1.37    |> Local_Theory.raw_theory f
    1.38    |> Local_Theory.target (synchronize_class_syntax [class]
    1.39        (base_sort (Proof_Context.theory_of lthy) class));
    1.40  
    1.41 -local
    1.42 -
    1.43  fun target_const class ((c, mx), (type_params, dict)) thy =
    1.44    let
    1.45      val morph = morphism thy class;
    1.46 @@ -478,8 +480,9 @@
    1.47  
    1.48  (* target *)
    1.49  
    1.50 -fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
    1.51 -    (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
    1.52 +fun define_overloaded (c, U) v (b_def, rhs) =
    1.53 +  Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
    1.54 +  ##>> AxClass.define_overloaded b_def (c, rhs))
    1.55    ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
    1.56    ##> Local_Theory.target synchronize_inst_syntax;
    1.57  
    1.58 @@ -603,8 +606,8 @@
    1.59      val (tycos, vs, sort) = read_multi_arity thy raw_arities;
    1.60      val sorts = map snd vs;
    1.61      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.62 -    fun after_qed results = Proof_Context.background_theory
    1.63 -      ((fold o fold) AxClass.add_arity results);
    1.64 +    fun after_qed results =
    1.65 +      Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
    1.66    in
    1.67      thy
    1.68      |> Proof_Context.init_global