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