src/Pure/Isar/class.ML
changeset 25163 f737a88a3248
parent 25146 c2a41f31cacb
child 25195 62638dcafe38
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 23 23:27:23 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 24 07:19:52 2007 +0200
     1.3 @@ -433,16 +433,13 @@
     1.4  
     1.5  (* updaters *)
     1.6  
     1.7 -fun add_class_data ((class, superclasses), (cs, base_sort, insttab, phi, intro)) thy =
     1.8 +fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
     1.9    let
    1.10 -    val inst = map
    1.11 -      (SOME o the o Symtab.lookup insttab o fst o fst)
    1.12 -        (Locale.parameters_of_expr thy (Locale.Locale class));
    1.13      val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
    1.14        (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
    1.15      val cs = (map o pairself) fst cs;
    1.16      val add_class = Graph.new_node (class,
    1.17 -        mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
    1.18 +        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
    1.19        #> fold (curry Graph.add_edge class) superclasses;
    1.20    in
    1.21      ClassData.map add_class thy
    1.22 @@ -738,10 +735,8 @@
    1.23      val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
    1.24        prep_spec thy raw_supclasses raw_includes_elems;
    1.25      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
    1.26 -    fun mk_inst class param_names cs =
    1.27 -      Symtab.empty
    1.28 -      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
    1.29 -           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
    1.30 +    fun mk_inst class cs =
    1.31 +      (map o apsnd o Term.map_type_tfree) (fn (v, _) => TFree (v, [class])) cs;
    1.32      fun fork_syntax (Element.Fixes xs) =
    1.33            fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
    1.34            #>> Element.Fixes
    1.35 @@ -785,7 +780,7 @@
    1.36        #-> (fn [(_, [class_intro])] =>
    1.37          add_class_data ((class, sups),
    1.38            (map fst params ~~ consts, base_sort,
    1.39 -            mk_inst class (map fst all_params) (map snd supconsts @ consts),
    1.40 +            mk_inst class (map snd supconsts @ consts),
    1.41                calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
    1.42        #> class_interpretation class axioms []
    1.43        )))))