# HG changeset patch
# User blanchet
# Date 1394718500 -3600
# Node ID 2ec2d06b9424d10c3c10daaa77e69dac32296979
# Parent  9cfea3ab002a3bc3793835160ab8ec9da82c4cf9
avoid name clash

diff -r 9cfea3ab002a -r 2ec2d06b9424 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Mar 13 14:48:20 2014 +0100
+++ b/src/HOL/SMT2.thy	Thu Mar 13 14:48:20 2014 +0100
@@ -90,7 +90,7 @@
 lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)"
   by simp
 
-lemma nat_int: "\<forall>n. nat (int n) = n" by simp
+lemma nat_int': "\<forall>n. nat (int n) = n" by simp
 lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
 lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
 
diff -r 9cfea3ab002a -r 2ec2d06b9424 src/HOL/Tools/SMT2/smt2_normalize.ML
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
@@ -296,15 +296,14 @@
   trigger_conv ctxt then_conv
   weight_conv weight ctxt
 
-fun gen_normalize1 ctxt weight thm =
-  thm
-  |> instantiate_elim
-  |> norm_def
-  |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
-  |> Drule.forall_intr_vars
-  |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
+fun gen_normalize1 ctxt weight =
+  instantiate_elim #>
+  norm_def #>
+  Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
+  Drule.forall_intr_vars #>
+  Conv.fconv_rule (gen_normalize1_conv ctxt weight) #>
   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
-  |> Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
+  Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
 
 fun gen_norm1_safe ctxt (i, (weight, thm)) =
   (case try (gen_normalize1 ctxt weight) thm of
@@ -375,7 +374,7 @@
 (** embedding of standard natural number operations into integer operations **)
 
 local
-  val nat_embedding = @{thms nat_int int_nat_nneg int_nat_neg}
+  val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg}
 
   val simple_nat_ops = [
     @{const less (nat)}, @{const less_eq (nat)},