src/Pure/axclass.ML
changeset 35960 536c07a2a0bc
parent 35896 487b267433b1
child 35961 00e48e1d9afd
     1.1 --- a/src/Pure/axclass.ML	Wed Mar 24 22:30:33 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Mar 25 21:14:15 2010 +0100
     1.3 @@ -37,9 +37,6 @@
     1.4    val param_of_inst: theory -> string * string -> string
     1.5    val inst_of_param: theory -> string -> (string * string) option
     1.6    val thynames_of_arity: theory -> class * string -> string list
     1.7 -  type cache
     1.8 -  val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
     1.9 -  val cache: cache
    1.10    val introN: string
    1.11    val axiomsN: string
    1.12  end;
    1.13 @@ -564,59 +561,4 @@
    1.14  
    1.15  end;
    1.16  
    1.17 -
    1.18 -
    1.19 -(** explicit derivations -- cached **)
    1.20 -
    1.21 -datatype cache = Types of (class * thm) list Typtab.table;
    1.22 -
    1.23 -local
    1.24 -
    1.25 -fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache;
    1.26 -fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache);
    1.27 -
    1.28 -fun derive_type _ (_, []) = []
    1.29 -  | derive_type thy (typ, sort) =
    1.30 -      let
    1.31 -        val certT = Thm.ctyp_of thy;
    1.32 -        val vars = Term.fold_atyps
    1.33 -            (fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
    1.34 -              | T as TVar (_, S) => insert (eq_fst op =) (T, S)
    1.35 -              | _ => I) typ [];
    1.36 -        val hyps = vars
    1.37 -          |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
    1.38 -        val ths = (typ, sort)
    1.39 -          |> Sorts.of_sort_derivation (Sign.classes_of thy)
    1.40 -           {class_relation =
    1.41 -              fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    1.42 -            type_constructor =
    1.43 -              fn a => fn dom => fn c =>
    1.44 -                let val Ss = map (map snd) dom and ths = maps (map fst) dom
    1.45 -                in ths MRS the_arity thy a (c, Ss) end,
    1.46 -            type_variable =
    1.47 -              the_default [] o AList.lookup (op =) hyps};
    1.48 -      in ths end;
    1.49 -
    1.50 -in
    1.51 -
    1.52 -fun of_sort thy (typ, sort) cache =
    1.53 -  let
    1.54 -    val sort' = filter (is_none o lookup_type cache typ) sort;
    1.55 -    val ths' = derive_type thy (typ, sort')
    1.56 -      handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
    1.57 -        Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
    1.58 -    val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
    1.59 -    val ths =
    1.60 -      sort |> map (fn c =>
    1.61 -        Goal.finish
    1.62 -          (Syntax.init_pretty_global thy)
    1.63 -          (the (lookup_type cache' typ c) RS
    1.64 -            Goal.init (Thm.cterm_of thy (Logic.mk_of_class (typ, c))))
    1.65 -        |> Thm.adjust_maxidx_thm ~1);
    1.66 -  in (ths, cache') end;
    1.67 -
    1.68  end;
    1.69 -
    1.70 -val cache = Types Typtab.empty;
    1.71 -
    1.72 -end;