# HG changeset patch
# User wenzelm
# Date 1430664278 -7200
# Node ID 3f61058a2de65ba8c5032417ff246842b19dd2f8
# Parent  755e11e2e15d2704aba6c7bde3afd155eaa1df0b
suppress formal sort-constraints, in accordance to norm_hhf_eqs;

diff -r 755e11e2e15d -r 3f61058a2de6 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun May 03 14:35:48 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun May 03 16:44:38 2015 +0200
@@ -138,17 +138,19 @@
     fn th =>
       let
         val th' = exp th;
-        val defs_asms = asms |> map (Thm.assume #> (fn asm =>
-          (case try (head_of_def o Thm.prop_of) asm of
-            NONE => (asm, false)
-          | SOME x =>
-              let val t = Free x in
-                (case try exp_term t of
-                  NONE => (asm, false)
-                | SOME u =>
-                    if t aconv u then (asm, false)
-                    else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
-              end)));
+        val defs_asms = asms
+          |> filter_out (Drule.is_sort_constraint o Thm.term_of)
+          |> map (Thm.assume #> (fn asm =>
+            (case try (head_of_def o Thm.prop_of) asm of
+              NONE => (asm, false)
+            | SOME x =>
+                let val t = Free x in
+                  (case try exp_term t of
+                    NONE => (asm, false)
+                  | SOME u =>
+                      if t aconv u then (asm, false)
+                      else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
+                end)));
       in (apply2 (map #1) (List.partition #2 defs_asms), th') end
   end;
 
diff -r 755e11e2e15d -r 3f61058a2de6 src/Pure/drule.ML
--- 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));