suppress formal sort-constraints, in accordance to norm_hhf_eqs;
authorwenzelm
Sun May 03 16:44:38 2015 +0200 (2015-05-03)
changeset 602403f61058a2de6
parent 60239 755e11e2e15d
child 60241 cde717a55db7
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
src/Pure/Isar/local_defs.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun May 03 14:35:48 2015 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sun May 03 16:44:38 2015 +0200
     1.3 @@ -138,17 +138,19 @@
     1.4      fn th =>
     1.5        let
     1.6          val th' = exp th;
     1.7 -        val defs_asms = asms |> map (Thm.assume #> (fn asm =>
     1.8 -          (case try (head_of_def o Thm.prop_of) asm of
     1.9 -            NONE => (asm, false)
    1.10 -          | SOME x =>
    1.11 -              let val t = Free x in
    1.12 -                (case try exp_term t of
    1.13 -                  NONE => (asm, false)
    1.14 -                | SOME u =>
    1.15 -                    if t aconv u then (asm, false)
    1.16 -                    else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
    1.17 -              end)));
    1.18 +        val defs_asms = asms
    1.19 +          |> filter_out (Drule.is_sort_constraint o Thm.term_of)
    1.20 +          |> map (Thm.assume #> (fn asm =>
    1.21 +            (case try (head_of_def o Thm.prop_of) asm of
    1.22 +              NONE => (asm, false)
    1.23 +            | SOME x =>
    1.24 +                let val t = Free x in
    1.25 +                  (case try exp_term t of
    1.26 +                    NONE => (asm, false)
    1.27 +                  | SOME u =>
    1.28 +                      if t aconv u then (asm, false)
    1.29 +                      else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
    1.30 +                end)));
    1.31        in (apply2 (map #1) (List.partition #2 defs_asms), th') end
    1.32    end;
    1.33  
     2.1 --- a/src/Pure/drule.ML	Sun May 03 14:35:48 2015 +0200
     2.2 +++ b/src/Pure/drule.ML	Sun May 03 16:44:38 2015 +0200
     2.3 @@ -93,6 +93,7 @@
     2.4    val dest_term: thm -> cterm
     2.5    val cterm_rule: (thm -> thm) -> cterm -> cterm
     2.6    val dummy_thm: thm
     2.7 +  val is_sort_constraint: term -> bool
     2.8    val sort_constraintI: thm
     2.9    val sort_constraint_eq: thm
    2.10    val with_subgoal: int -> (thm -> thm) -> thm -> thm
    2.11 @@ -647,6 +648,9 @@
    2.12  
    2.13  (* sort_constraint *)
    2.14  
    2.15 +fun is_sort_constraint (Const ("Pure.sort_constraint", _) $ Const ("Pure.type", _)) = true
    2.16 +  | is_sort_constraint _ = false;
    2.17 +
    2.18  val sort_constraintI =
    2.19    store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
    2.20      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));