1.1 --- a/src/Pure/Isar/class.ML	Wed Jul 30 07:33:57 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Jul 30 07:33:58 2008 +0200
     1.3 @@ -301,11 +301,20 @@
     1.4        | NONE => I;
     1.5  
     1.6      (*dynamic parts of morphism*)
     1.7 +    fun avoid_a thy thm =
     1.8 +      let
     1.9 +        val tvars = Term.add_tvars (Thm.prop_of thm) [];
    1.10 +        val thm' = case AList.lookup (op =) tvars (Name.aT, 0)
    1.11 +         of SOME sort => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o rpair sort o rpair 0)
    1.12 +              (Name.aT, Name.variant (map (fst o fst) tvars) Name.aT)], []) thm
    1.13 +          | NONE => thm;
    1.14 +      in thm' end;
    1.15      fun rew_term thy defs = Pattern.rewrite_term thy
    1.16        (map (Logic.dest_equals o Thm.prop_of) defs) [];
    1.17      fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs
    1.18        #> map_types subst_typ;
    1.19 -    fun subst_thm thy defs = Drule.standard' #> instantiate thy [class] #> lift_axiom
    1.20 +    fun subst_thm thy defs = Drule.zero_var_indexes #> avoid_a thy
    1.21 +      #> Drule.standard' #> instantiate thy [class] #> lift_axiom
    1.22        #> MetaSimplifier.rewrite_rule defs;
    1.23      fun morphism thy defs =
    1.24        Morphism.typ_morphism subst_typ
    1.25 @@ -630,9 +639,6 @@
    1.26      val class = Sign.full_name thy bname;
    1.27      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
    1.28        prep_spec thy raw_supclasses raw_elems;
    1.29 -    fun assms_of thy class =
    1.30 -      Locale.elems thy class
    1.31 -      |> map_filter (fn Element.Notes (_, facts) => SOME facts | _ => NONE);
    1.32    in
    1.33      thy
    1.34      |> Locale.add_locale_i "" bname mergeexpr elems
    1.35 @@ -644,10 +650,10 @@
    1.36      #-> (fn (morphism, axiom, assm_intro, of_class) =>
    1.37          add_class_data ((class, sups), (params, base_sort,
    1.38            map snd param_map, morphism, axiom, assm_intro, of_class))
    1.39 -    (*#> `(fn thy => assms_of thy class)
    1.40 -    #-> (fn assms => fold_map (note class Thm.assumptionK) assms
    1.41 +    (*#> `(fn thy => Locale.facts_of thy class)
    1.42 +    #-> (fn facts => fold_map (note class Thm.assumptionK) facts
    1.43      #> snd*)
    1.44 -    #> class_interpretation class (the_list axiom) []))(*)*)
    1.45 +    #> class_interpretation class (the_list axiom) []))
    1.46      |> init class
    1.47      |> pair class
    1.48    end;