src/Pure/drule.ML
 changeset 56245 84fc7dfa3cd4 parent 52467 24c6ddb48cb8 child 56436 30ccec1e82fb
```     1.1 --- a/src/Pure/drule.ML	Fri Mar 21 15:12:03 2014 +0100
1.2 +++ b/src/Pure/drule.ML	Fri Mar 21 20:33:56 2014 +0100
1.3 @@ -126,7 +126,7 @@
1.4  (* A1==>...An==>B  goes to B, where B is not an implication *)
1.5  fun strip_imp_concl ct =
1.6    (case Thm.term_of ct of
1.7 -    Const ("==>", _) \$ _ \$ _ => strip_imp_concl (Thm.dest_arg ct)
1.8 +    Const ("Pure.imp", _) \$ _ \$ _ => strip_imp_concl (Thm.dest_arg ct)
1.9    | _ => ct);
1.10
1.11  (*The premises of a theorem, as a cterm list*)
1.12 @@ -706,7 +706,7 @@
1.13  val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
1.14
1.15  fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
1.16 -  | is_norm_hhf (Const ("==>", _) \$ _ \$ (Const ("all", _) \$ _)) = false
1.17 +  | is_norm_hhf (Const ("Pure.imp", _) \$ _ \$ (Const ("Pure.all", _) \$ _)) = false
1.18    | is_norm_hhf (Abs _ \$ _) = false
1.19    | is_norm_hhf (t \$ u) = is_norm_hhf t andalso is_norm_hhf u
1.20    | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
```