1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -1205,7 +1205,7 @@
     1.4  fun non_trivial_term_consts t = fold_aterms
     1.5    (fn Const (c, _) =>
     1.6        if c = @{const_name Trueprop} orelse c = @{const_name All}
     1.7 -        orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
     1.8 +        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
     1.9        then I else insert (op =) c
    1.10      | _ => I) t [];
    1.11  
    1.12 @@ -1217,7 +1217,7 @@
    1.13                 | @{const_name HOL.implies} => insert (op =) "==>" cs
    1.14                 | @{const_name All} => cs
    1.15                 | "all" => cs
    1.16 -               | @{const_name "op &"} => cs
    1.17 +               | @{const_name HOL.conj} => cs
    1.18                 | @{const_name Trueprop} => cs
    1.19                 | _ => insert (op =) c cs)
    1.20            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    1.21 @@ -1521,7 +1521,7 @@
    1.22          val th1 = norm_hyps th1
    1.23          val th2 = norm_hyps th2
    1.24          val (l,r) = case concl_of th of
    1.25 -                        _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
    1.26 +                        _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
    1.27                        | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
    1.28          val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
    1.29          val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2