# HG changeset patch
# User wenzelm
# Date 1519392779 -3600
# Node ID 8c4806fe827f8317ea76a84913c353a41c680bf3
# Parent  2d9918f5b33cb45c15ad842310efe96053de1d37
tuned signature -- eliminated clones;

diff -r 2d9918f5b33c -r 8c4806fe827f src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 14:12:48 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 14:32:59 2018 +0100
@@ -187,7 +187,7 @@
           let
             val [rty, rty'] = binder_types typ
           in
-            if Term.is_TVar rty andalso is_Type rty' then
+            if Term.is_TVar rty andalso Term.is_Type rty' then
               (xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst
             else
               subst
@@ -472,7 +472,7 @@
     if same_type_constrs (rty, qty) then
       forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
     else
-      if is_Type qty then
+      if Term.is_Type qty then
         if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
         else
           let
diff -r 2d9918f5b33c -r 8c4806fe827f src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 14:12:48 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 14:32:59 2018 +0100
@@ -25,7 +25,6 @@
   val get_args: int -> term -> term list
   val strip_args: int -> term -> term
   val all_args_conv: conv -> conv
-  val is_Type: typ -> bool
   val same_type_constrs: typ * typ -> bool
   val Targs: typ -> typ list
   val Tname: typ -> string
@@ -108,9 +107,6 @@
 
 fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
 
-fun is_Type (Type _) = true
-  | is_Type _ = false
-
 fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
   | same_type_constrs _ = false
 
diff -r 2d9918f5b33c -r 8c4806fe827f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 23 14:12:48 2018 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 23 14:32:59 2018 +0100
@@ -83,7 +83,6 @@
   val const_match : theory -> (string * typ) * (string * typ) -> bool
   val term_match : theory -> term * term -> bool
   val frac_from_term_pair : typ -> term -> term -> term
-  val is_TFree : typ -> bool
   val is_fun_type : typ -> bool
   val is_set_type : typ -> bool
   val is_fun_or_set_type : typ -> bool
@@ -478,9 +477,6 @@
           | n2 => Const (@{const_name divide}, T --> T --> T)
                   $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
 
-fun is_TFree (TFree _) = true
-  | is_TFree _ = false
-
 fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
 
diff -r 2d9918f5b33c -r 8c4806fe827f src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Feb 23 14:12:48 2018 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Feb 23 14:32:59 2018 +0100
@@ -38,9 +38,6 @@
 
 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
 
-fun is_Type (Type _) = true
-  | is_Type _ = false
-
 fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
diff -r 2d9918f5b33c -r 8c4806fe827f src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Feb 23 14:12:48 2018 +0100
+++ b/src/Pure/term.ML	Fri Feb 23 14:32:59 2018 +0100
@@ -34,14 +34,16 @@
   val no_dummyT: typ -> typ
   val --> : typ * typ -> typ
   val ---> : typ list * typ -> typ
+  val is_Type: typ -> bool
+  val is_TFree: typ -> bool
+  val is_TVar: typ -> bool
   val dest_Type: typ -> string * typ list
+  val dest_TFree: typ -> string * sort
   val dest_TVar: typ -> indexname * sort
-  val dest_TFree: typ -> string * sort
   val is_Bound: term -> bool
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
-  val is_TVar: typ -> bool
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
@@ -246,12 +248,29 @@
 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
 val op ---> = Library.foldr (op -->);
 
+
+(** Discriminators **)
+
+fun is_Type (Type _) = true
+  | is_Type _ = false;
+
+fun is_TFree (TFree _) = true
+  | is_TFree _ = false;
+
+fun is_TVar (TVar _) = true
+  | is_TVar _ = false;
+
+
+(** Destructors **)
+
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
+
+fun dest_TFree (TFree x) = x
+  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
+
 fun dest_TVar (TVar x) = x
   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
-fun dest_TFree (TFree x) = x
-  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
 
 
 (** Discriminators **)
@@ -268,9 +287,6 @@
 fun is_Var (Var _) = true
   | is_Var _ = false;
 
-fun is_TVar (TVar _) = true
-  | is_TVar _ = false;
-
 
 (** Destructors **)