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