--- a/src/CCL/CCL.thy Wed Dec 01 15:02:39 2010 +0100
+++ b/src/CCL/CCL.thy Wed Dec 01 15:03:44 2010 +0100
@@ -233,7 +233,7 @@
| arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
| arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
val T = Sign.the_const_type thy (Sign.intern_const thy sy);
- val arity = length (fst (strip_type T))
+ val arity = length (binder_types T)
in sy ^ (arg_str arity name "") end
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Dec 01 15:03:44 2010 +0100
@@ -274,7 +274,7 @@
fun perm_arg (dt, x) =
let val T = type_of x
in if is_rec_type dt then
- let val (Us, _) = strip_type T
+ let val Us = binder_types T
in list_abs (map (pair "x") Us,
Free (nth perm_names_types' (body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Dec 01 15:03:44 2010 +0100
@@ -334,14 +334,14 @@
val t :: ts2 = drop i ts;
val names = List.foldr OldTerm.add_term_names
(map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
- val (Ts, dT) = split_last (take (i+1) (fst (strip_type T)));
+ val (Ts, dT) = split_last (take (i+1) (binder_types T));
fun pcase [] [] [] gr = ([], gr)
| pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
let
val j = length cargs;
val xs = Name.variant_list names (replicate j "x");
- val Us' = take j (fst (strip_type U));
+ val Us' = take j (binder_types U);
val frees = map2 (curry Free) xs Us';
val (cp, gr0) = invoke_codegen thy defs dep module false
(list_comb (Const (cname, Us' ---> dT), frees)) gr;
@@ -385,26 +385,33 @@
(* code generators for terms and types *)
-fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
- (c as Const (s, T), ts) =>
- (case Datatype_Data.info_of_case thy s of
+fun datatype_codegen thy defs dep module brack t gr =
+ (case strip_comb t of
+ (c as Const (s, T), ts) =>
+ (case Datatype_Data.info_of_case thy s of
SOME {index, descr, ...} =>
- if is_some (get_assoc_code thy (s, T)) then NONE else
- SOME (pretty_case thy defs dep module brack
- (#3 (the (AList.lookup op = descr index))) c ts gr )
- | NONE => case (Datatype_Data.info_of_constr thy (s, T), strip_type T) of
- (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
- if is_some (get_assoc_code thy (s, T)) then NONE else
- let
- val SOME (tyname', _, constrs) = AList.lookup op = descr index;
- val SOME args = AList.lookup op = constrs s
- in
- if tyname <> tyname' then NONE
- else SOME (pretty_constr thy defs
- dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
- end
- | _ => NONE)
- | _ => NONE);
+ if is_some (get_assoc_code thy (s, T)) then NONE
+ else
+ SOME (pretty_case thy defs dep module brack
+ (#3 (the (AList.lookup op = descr index))) c ts gr)
+ | NONE =>
+ (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
+ (SOME {index, descr, ...}, U as Type (tyname, _)) =>
+ if is_some (get_assoc_code thy (s, T)) then NONE
+ else
+ let
+ val SOME (tyname', _, constrs) = AList.lookup op = descr index;
+ val SOME args = AList.lookup op = constrs s;
+ in
+ if tyname <> tyname' then NONE
+ else
+ SOME
+ (pretty_constr thy defs
+ dep module brack args c ts
+ (snd (invoke_tycodegen thy defs dep module false U gr)))
+ end
+ | _ => NONE))
+ | _ => NONE);
fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
(case Datatype_Data.get_info thy s of
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 01 15:03:44 2010 +0100
@@ -72,7 +72,7 @@
fun info_of_constr thy (c, T) =
let
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
- val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
+ val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
val default = if null tab then NONE
else SOME (snd (Library.last_elem tab))
(*conservative wrt. overloaded constructors*);
@@ -387,7 +387,7 @@
fun type_of_constr (cT as (_, T)) =
let
val frees = OldTerm.typ_tfrees T;
- val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
+ val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
handle TYPE _ => no_constr cT
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
val _ = if length frees <> length vs then no_constr cT else ();
@@ -412,8 +412,8 @@
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
val cs = map (apsnd (map norm_constr)) raw_cs;
- val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
- o fst o strip_type;
+ val dtyps_of_typ =
+ map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
val dt_names = map fst cs;
fun mk_spec (i, (tyco, constr)) = (i, (tyco,
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 01 15:03:44 2010 +0100
@@ -385,7 +385,7 @@
fun mk_clause ((f, g), (cname, _)) =
let
- val (Ts, _) = strip_type (fastype_of f);
+ val Ts = binder_types (fastype_of f);
val tnames = Name.variant_list used (make_tnames Ts);
val frees = map Free (tnames ~~ Ts)
in
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 15:03:44 2010 +0100
@@ -25,7 +25,7 @@
fun prf_of thm =
Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
+fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 15:03:44 2010 +0100
@@ -485,7 +485,7 @@
fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
+fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
| is_predT _ = false
(*** check if a term contains only constructor functions ***)
--- a/src/HOL/Tools/recfun_codegen.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Wed Dec 01 15:03:44 2010 +0100
@@ -34,7 +34,8 @@
fun avoid_value thy [thm] =
let val (_, T) = Code.const_typ_eqn thy thm
- in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
+ in
+ if null (Term.add_tvarsT T []) orelse null (binder_types T)
then [thm]
else [Code.expand_eta thy 1 thm]
end
--- a/src/HOL/Tools/record.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/HOL/Tools/record.ML Wed Dec 01 15:03:44 2010 +0100
@@ -1869,7 +1869,7 @@
(fn _ => fn eq_def => tac eq_def) eq_def)
|-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
|> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
- |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+ |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
end;
--- a/src/Pure/Isar/code.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Pure/Isar/code.ML Wed Dec 01 15:03:44 2010 +0100
@@ -358,7 +358,7 @@
of SOME ty => ty
| NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
-fun args_number thy = length o fst o strip_type o const_typ thy;
+fun args_number thy = length o binder_types o const_typ thy;
fun subst_signature thy c ty =
let
@@ -391,7 +391,7 @@
fun last_typ c_ty ty =
let
val tfrees = Term.add_tfreesT ty [];
- val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
+ val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
handle TYPE _ => no_constr thy "bad type" c_ty
val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
val _ = if has_duplicates (eq_fst (op =)) vs
@@ -420,7 +420,7 @@
val the_v = the o AList.lookup (op =) (vs ~~ vs');
val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
val (vs'', _) = logical_typscheme thy (c, ty');
- in (c, (vs'', (fst o strip_type) ty')) end;
+ in (c, (vs'', binder_types ty')) end;
val c' :: cs' = map (analyze_constructor thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
val vs = Name.names Name.context Name.aT sorts;
@@ -444,7 +444,7 @@
| _ => error ("Not an abstract type: " ^ tyco);
fun get_type_of_constr_or_abstr thy c =
- case (snd o strip_type o const_typ thy) c
+ case (body_type o const_typ thy) c
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
| _ => NONE;
@@ -517,7 +517,7 @@
| check n (Const (c_ty as (c, ty))) =
if allow_pats then let
val c' = AxClass.unoverload_const thy c_ty
- in if n = (length o fst o strip_type o subst_signature thy c') ty
+ in if n = (length o binder_types o subst_signature thy c') ty
then if allow_consts orelse is_constr thy c'
then ()
else bad (quote c ^ " is not a constructor, on left hand side of equation")
@@ -1139,7 +1139,7 @@
val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
- val Ts = (fst o strip_type) T;
+ val Ts = binder_types T;
val T_cong = nth Ts pos;
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
--- a/src/Pure/Proof/extraction.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Dec 01 15:03:44 2010 +0100
@@ -135,11 +135,13 @@
val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
-fun relevant_vars types prop = List.foldr (fn
- (Var ((a, _), T), vs) => (case strip_type T of
- (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
- | _ => vs)
- | (_, vs) => vs) [] (vars_of prop);
+fun relevant_vars types prop =
+ List.foldr
+ (fn (Var ((a, _), T), vs) =>
+ (case body_type T of
+ Type (s, _) => if member (op =) types s then a :: vs else vs
+ | _ => vs)
+ | (_, vs) => vs) [] (vars_of prop);
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
--- a/src/Pure/codegen.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Pure/codegen.ML Wed Dec 01 15:03:44 2010 +0100
@@ -664,7 +664,7 @@
NONE =>
let
val _ = message ("expanding definition of " ^ s);
- val (Ts, _) = strip_type U;
+ val Ts = binder_types U;
val (args', rhs') =
if not (null args) orelse null Ts then (args, rhs) else
let val v = Free (new_name rhs "x", hd Ts)
--- a/src/Pure/term.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Pure/term.ML Wed Dec 01 15:03:44 2010 +0100
@@ -712,7 +712,7 @@
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
in ((v, T) :: vs, t') end;
val ((vs1, t'), (k', used')) = strip_abs t (k, used);
- val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
+ val Ts = fst (chop k' (binder_types (fastype_of t')));
val (vs2, t'') = expand_eta Ts t' used';
in (vs1 @ vs2, t'') end;
--- a/src/Tools/Code/code_thingol.ML Wed Dec 01 15:02:39 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Dec 01 15:03:44 2010 +0100
@@ -710,7 +710,7 @@
else ()
val arg_typs = Sign.const_typargs thy (c, ty);
val sorts = Code_Preproc.sortargs eqngr c;
- val function_typs = (fst o Term.strip_type) ty;
+ val function_typs = Term.binder_types ty;
in
ensure_const thy algbr eqngr permissive c
##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
@@ -724,7 +724,7 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
- fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
+ fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
fun mk_constr c t = let val n = Code.args_number thy c