--- 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
--- 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
--- 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
--- 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)
--- 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 **)