# HG changeset patch
# User paulson
# Date 913975285 -3600
# Node ID c8c69a4a7762124b8550a580b1be6b5d4232d8fb
# Parent  c4e62bab69bd90c5f1718e91aabc94caf7de6fa2
moved dest_Type to term.ML from HOL/Tools/primrec_package

diff -r c4e62bab69bd -r c8c69a4a7762 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 18 11:00:46 1998 +0100
+++ b/src/Pure/term.ML	Fri Dec 18 11:01:25 1998 +0100
@@ -40,6 +40,7 @@
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
+  val dest_Type: typ -> string * typ list
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
@@ -188,13 +189,7 @@
              | TFree of string * sort
 	     | TVar  of indexname * sort;
 
-fun S --> T = Type("fun",[S,T]);
-
-(*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
-val op ---> = foldr (op -->);
-
-
-(*terms.  Bound variables are indicated by depth number.
+(*Terms.  Bound variables are indicated by depth number.
   Free variables, (scheme) variables and constants have names.
   An term is "closed" if every bound variable of level "lev"
   is enclosed by at least "lev" abstractions. 
@@ -232,6 +227,17 @@
 *)
 
 
+(** Types **)
+
+fun S --> T = Type("fun",[S,T]);
+
+(*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
+val op ---> = foldr (op -->);
+
+fun dest_Type (Type x) = x
+  | dest_Type T = raise TYPE ("dest_Type", [T], []);
+
+
 (** Discriminators **)
 
 fun is_Const (Const _) = true