--- a/src/Pure/drule.ML Sun May 03 14:35:48 2015 +0200
+++ b/src/Pure/drule.ML Sun May 03 16:44:38 2015 +0200
@@ -93,6 +93,7 @@
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
val dummy_thm: thm
+ val is_sort_constraint: term -> bool
val sort_constraintI: thm
val sort_constraint_eq: thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
@@ -647,6 +648,9 @@
(* sort_constraint *)
+fun is_sort_constraint (Const ("Pure.sort_constraint", _) $ Const ("Pure.type", _)) = true
+ | is_sort_constraint _ = false;
+
val sort_constraintI =
store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));