src/Pure/Isar/class.ML
changeset 25239 3d6abdd10382
parent 25210 5b5659801257
child 25268 58146cb7bf44
     1.1 --- a/src/Pure/Isar/class.ML	Tue Oct 30 12:14:24 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Oct 30 14:39:35 2007 +0100
     1.3 @@ -450,23 +450,21 @@
     1.4      ClassData.map add_class thy
     1.5    end;
     1.6  
     1.7 -fun register_operation class (c, ((t, some_t_rev), some_def)) thy =
     1.8 +fun register_operation class (c, ((t, t_rev), some_def)) thy =
     1.9    let
    1.10      val ty = Sign.the_const_constraint thy c;
    1.11      val typargs = Sign.const_typargs thy (c, ty);
    1.12      val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
    1.13 -    fun mk_uncheck t_rev =
    1.14 -      let
    1.15 -        val t_rev' = map_types Type.strip_sorts t_rev;
    1.16 -        val ty' = Term.fastype_of t_rev';
    1.17 -      in (t_rev', Const (c, ty')) end;
    1.18 -    val some_t_rev' = Option.map mk_uncheck some_t_rev;
    1.19 +    val prep_typ = map_atyps
    1.20 +      (fn TVar (vi as (v, _), _) => if Name.aT = v then TFree (v, []) else TVar (vi, []))
    1.21 +    val t_rev' = map_types prep_typ t_rev;
    1.22 +    val ty' = Term.fastype_of t_rev';
    1.23    in
    1.24      thy
    1.25      |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
    1.26        (fn (defs, (operations, unchecks)) =>
    1.27          (fold cons (the_list some_def) defs,
    1.28 -          ((c, (t, (ty, typidx))) :: operations, fold cons (the_list some_t_rev') unchecks)))
    1.29 +          ((c, (t, (ty, typidx))) :: operations, (t_rev', Const (c, ty')) :: unchecks)))
    1.30    end;
    1.31  
    1.32  
    1.33 @@ -864,20 +862,20 @@
    1.34      val prfx = class_prefix class;
    1.35      val thy' = thy |> Sign.add_path prfx;
    1.36      val phi = morphism thy' class;
    1.37 -    val base_sort = (#base_sort o the_class_data thy) class;
    1.38  
    1.39      val c' = Sign.full_name thy' c;
    1.40 -    val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict;
    1.41 -    val ty' = Term.fastype_of dict';
    1.42 +    val dict' = Morphism.term phi dict;
    1.43 +    val dict_def = map_types Logic.unvarifyT dict';
    1.44 +    val ty' = Term.fastype_of dict_def;
    1.45      val ty'' = Type.strip_sorts ty';
    1.46 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict');
    1.47 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
    1.48    in
    1.49      thy'
    1.50      |> Sign.declare_const pos (c, ty'', mx) |> snd
    1.51      |> Thm.add_def false (c, def_eq)
    1.52      |>> Thm.symmetric
    1.53      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
    1.54 -          #> register_operation class (c', ((dict, SOME dict'), SOME (Thm.varifyT def))))
    1.55 +          #> register_operation class (c', ((dict, dict'), SOME (Thm.varifyT def))))
    1.56      |> Sign.restore_naming thy
    1.57      |> Sign.add_const_constraint (c', SOME ty')
    1.58    end;
    1.59 @@ -894,13 +892,13 @@
    1.60      val c' = Sign.full_name thy' c;
    1.61      val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
    1.62      val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
    1.63 -    val ty' = (Logic.unvarifyT o Term.fastype_of) rhs';
    1.64 +    val ty' = Logic.unvarifyT (Term.fastype_of rhs');
    1.65    in
    1.66      thy'
    1.67      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
    1.68      |> Sign.add_const_constraint (c', SOME ty')
    1.69      |> Sign.notation true prmode [(Const (c', ty'), mx)]
    1.70 -    |> register_operation class (c', ((rhs, NONE), NONE))
    1.71 +    |> register_operation class (c', ((rhs, rhs'), NONE))
    1.72      |> Sign.restore_naming thy
    1.73    end;
    1.74