# HG changeset patch
# User wenzelm
# Date 1291212224 -3600
# Node ID 5895c525739da4af28afb5ceb28288c631e1ffcf
# Parent  b254814a094c9c42cafb75a2f51cea5a10ceb2c2
more direct use of binder_types/body_type;

diff -r b254814a094c -r 5895c525739d src/CCL/CCL.thy
--- 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")
diff -r b254814a094c -r 5895c525739d src/HOL/Nominal/nominal_datatype.ML
--- 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) =>
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/Datatype/datatype_codegen.ML
--- 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
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/Datatype/datatype_data.ML
--- 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,
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/Datatype/datatype_prop.ML
--- 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
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/Datatype/datatype_realizer.ML
--- 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 _ = "";
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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 ***)
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/recfun_codegen.ML
--- 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
diff -r b254814a094c -r 5895c525739d src/HOL/Tools/record.ML
--- 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;
 
 
diff -r b254814a094c -r 5895c525739d src/Pure/Isar/code.ML
--- 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);
diff -r b254814a094c -r 5895c525739d src/Pure/Proof/extraction.ML
--- 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 _ = "";
diff -r b254814a094c -r 5895c525739d src/Pure/codegen.ML
--- 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)
diff -r b254814a094c -r 5895c525739d src/Pure/term.ML
--- 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;
 
diff -r b254814a094c -r 5895c525739d src/Tools/Code/code_thingol.ML
--- 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