# HG changeset patch
# User haftmann
# Date 1256556239 -3600
# Node ID 3802b3b7845f68f3068efc869afed7d60e839147
# Parent  32a7a25fd918204e2a0db3d95f1d84608d02ac1b# Parent  616be6d7997ec55bbec68bd1c8f8437ba6d85caf
merged

diff -r 32a7a25fd918 -r 3802b3b7845f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 26 12:02:06 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Oct 26 12:23:59 2009 +0100
@@ -1827,24 +1827,28 @@
 text {* Code equations *}
 
 lemma [code]:
-  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
-    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
-    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
-    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
+  shows "(False \<Longrightarrow> P) \<equiv> Trueprop True" 
+    and "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" 
+    and "(P \<Longrightarrow> False) \<equiv> Trueprop (\<not> P)"
+    and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" by (auto intro!: equal_intr_rule)
 
 lemma [code]:
-  shows "False \<and> x \<longleftrightarrow> False"
-    and "True \<and> x \<longleftrightarrow> x"
-    and "x \<and> False \<longleftrightarrow> False"
-    and "x \<and> True \<longleftrightarrow> x" by simp_all
+  shows "False \<and> P \<longleftrightarrow> False"
+    and "True \<and> P \<longleftrightarrow> P"
+    and "P \<and> False \<longleftrightarrow> False"
+    and "P \<and> True \<longleftrightarrow> P" by simp_all
 
 lemma [code]:
-  shows "False \<or> x \<longleftrightarrow> x"
-    and "True \<or> x \<longleftrightarrow> True"
-    and "x \<or> False \<longleftrightarrow> x"
-    and "x \<or> True \<longleftrightarrow> True" by simp_all
+  shows "False \<or> P \<longleftrightarrow> P"
+    and "True \<or> P \<longleftrightarrow> True"
+    and "P \<or> False \<longleftrightarrow> P"
+    and "P \<or> True \<longleftrightarrow> True" by simp_all
 
-declare imp_conv_disj [code, code_unfold_post]
+lemma [code]:
+  shows "(False \<longrightarrow> P) \<longleftrightarrow> True"
+    and "(True \<longrightarrow> P) \<longleftrightarrow> P"
+    and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+    and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
 
 instantiation itself :: (type) eq
 begin
diff -r 32a7a25fd918 -r 3802b3b7845f src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Oct 26 12:02:06 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Oct 26 12:23:59 2009 +0100
@@ -5,7 +5,7 @@
 header {* Implementation of finite sets by lists *}
 
 theory Executable_Set
-imports Main Fset
+imports Main Fset SML_Quickcheck
 begin
 
 subsection {* Preprocessor setup *}
diff -r 32a7a25fd918 -r 3802b3b7845f src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Oct 26 12:02:06 2009 +0100
+++ b/src/Pure/Thy/term_style.ML	Mon Oct 26 12:23:59 2009 +0100
@@ -54,10 +54,11 @@
       >> fold I
   || Scan.succeed I));
 
-val parse_bare = Args.context :|-- (fn ctxt => Scan.lift Args.liberal_name
+val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style.";
+  Scan.lift Args.liberal_name
   >> (fn name => fst (Args.context_syntax "style"
        (Scan.lift (the_style (ProofContext.theory_of ctxt) name))
-          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))));
+          (Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt)))));
 
 
 (* predefined styles *)
@@ -84,10 +85,13 @@
 fun style_parm_premise i = Scan.succeed (fn ctxt => fn t =>
   let
     val i_str = string_of_int i;
+    val _ = Output.legacy_feature (quote ("prem" ^ i_str)
+      ^ " term style encountered; use explicit argument syntax "
+      ^ quote ("prem " ^ i_str) ^ " instead.");
     val prems = Logic.strip_imp_prems t;
   in
     if i <= length prems then nth prems (i - 1)
-    else error ("Not enough premises for prem" ^ string_of_int i ^
+    else error ("Not enough premises for prem" ^ i_str ^
       " in propositon: " ^ Syntax.string_of_term ctxt t)
   end);
 
diff -r 32a7a25fd918 -r 3802b3b7845f src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 26 12:02:06 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 26 12:23:59 2009 +0100
@@ -399,7 +399,7 @@
 fun expand_eta thy k thm =
   let
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
-    val (head, args) = strip_comb lhs;
+    val (_, args) = strip_comb lhs;
     val l = if k = ~1
       then (length o fst o strip_abs) rhs
       else Int.max (0, k - length args);