tuned
authorhaftmann
Mon Nov 29 11:38:59 2010 +0100 (2010-11-29)
changeset 408033f66ea311d44
parent 40800 330eb65c9469
child 40804 c8494f89690a
tuned
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Sun Nov 28 21:07:28 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Nov 29 11:38:59 2010 +0100
     1.3 @@ -383,7 +383,7 @@
     1.4  fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
     1.5    ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
     1.6  
     1.7 -fun ty_sorts thy (c, raw_ty) =
     1.8 +fun analyze_constructor thy (c, raw_ty) =
     1.9    let
    1.10      val _ = Thm.cterm_of thy (Const (c, raw_ty));
    1.11      val ty = subst_signature thy c raw_ty;
    1.12 @@ -418,10 +418,10 @@
    1.13      fun inst vs' (c, (vs, ty)) =
    1.14        let
    1.15          val the_v = the o AList.lookup (op =) (vs ~~ vs');
    1.16 -        val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
    1.17 +        val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
    1.18          val (vs'', _) = logical_typscheme thy (c, ty');
    1.19        in (c, (vs'', (fst o strip_type) ty')) end;
    1.20 -    val c' :: cs' = map (ty_sorts thy) cs;
    1.21 +    val c' :: cs' = map (analyze_constructor thy) cs;
    1.22      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    1.23      val vs = Name.names Name.context Name.aT sorts;
    1.24      val cs''' = map (inst vs) cs'';
    1.25 @@ -676,7 +676,7 @@
    1.26      val _ = (fst o dest_Var) param
    1.27        handle TERM _ => bad "Not an abstype certificate";
    1.28      val _ = if param = rhs then () else bad "Not an abstype certificate";
    1.29 -    val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
    1.30 +    val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
    1.31      val ty = domain_type ty';
    1.32      val (vs', _) = logical_typscheme thy (abs, ty');
    1.33    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    1.34 @@ -705,8 +705,8 @@
    1.35        (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
    1.36      val inst = map2 (fn (v, sort) => fn (_, sort') =>
    1.37        (((v, 0), sort), TFree (v, sort'))) vs mapping;
    1.38 -    val subst = (map_types o map_atyps)
    1.39 -      (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
    1.40 +    val subst = (map_types o map_type_tfree)
    1.41 +      (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
    1.42    in
    1.43      thm
    1.44      |> Thm.varifyT_global