merged
authorwenzelm
Fri, 21 Oct 2011 16:21:12 +0200
changeset 45237 769c4cbcd319
parent 45236 ac4a2a66707d (diff)
parent 45229 84f0b18a6e6e (current diff)
child 45239 ccea94064585
merged
--- a/NEWS	Fri Oct 21 11:27:21 2011 +0200
+++ b/NEWS	Fri Oct 21 16:21:12 2011 +0200
@@ -13,6 +13,9 @@
  'code_library', 'consts_code', 'types_code' have been discontinued.
   Use commands of the generic code generator instead. INCOMPATIBILITY.
 
+* Redundant attribute 'code_inline' has been discontinued. Use 'code_unfold'
+instead. INCOMPATIBILITY.
+
 *** HOL ***
 
 * 'Transitive_Closure.ntrancl': bounded transitive closure on relations.
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -1744,8 +1744,9 @@
     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
-    @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
+    @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
     @{attribute_def (HOL) code_post} & : & @{text attribute} \\
+    @{attribute_def (HOL) code_unfold_post} & : & @{text attribute} \\
     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -1790,12 +1791,15 @@
     @@{command (HOL) code_datatype} ( const + )
     ;
 
-    @@{attribute (HOL) code_inline} ( 'del' ) ?
+    @@{attribute (HOL) code_unfold} ( 'del' ) ?
     ;
 
     @@{attribute (HOL) code_post} ( 'del' ) ?
     ;
 
+    @@{attribute (HOL) code_unfold_post}
+    ;
+
     @@{command (HOL) code_thms} ( constexpr + ) ?
     ;
 
@@ -1887,14 +1891,18 @@
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
-  \item @{attribute (HOL) code_inline} declares (or with option
-  ``@{text "del"}'' removes) inlining theorems which are applied as
+  \item @{attribute (HOL) code_unfold} declares (or with option
+  ``@{text "del"}'' removes) theorems which are applied as
   rewrite rules to any code equation during preprocessing.
 
   \item @{attribute (HOL) code_post} declares (or with option ``@{text
   "del"}'' removes) theorems which are applied as rewrite rules to any
   result of an evaluation.
 
+  \item @{attribute (HOL) code_unfold_post} declares equations which are
+  applied as rewrite rules to any code equation during preprocessing,
+  and symmetrically to any result of an evaluation.
+  
   \item @{command (HOL) "print_codeproc"} prints the setup of the code
   generator preprocessor.
 
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 21 11:27:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 21 16:21:12 2011 +0200
@@ -2543,8 +2543,9 @@
     \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}} & : & \isa{attribute} \\
+    \indexdef{HOL}{attribute}{code\_unfold}\hypertarget{attribute.HOL.code-unfold}{\hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\
+    \indexdef{HOL}{attribute}{code\_unfold\_post}\hypertarget{attribute.HOL.code-unfold-post}{\hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\
     \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -2654,7 +2655,7 @@
 \rail@endplus
 \rail@end
 \rail@begin{2}{}
-\rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
+\rail@term{\hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{del}}[]
@@ -2667,6 +2668,9 @@
 \rail@term{\isa{del}}[]
 \rail@endbar
 \rail@end
+\rail@begin{1}{}
+\rail@term{\hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
+\rail@end
 \rail@begin{3}{}
 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
 \rail@bar
@@ -2919,13 +2923,17 @@
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on
   selected code equations and code generator datatypes.
 
-  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option
-  ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as
+  \item \hyperlink{attribute.HOL.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} declares (or with option
+  ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as
   rewrite rules to any code equation during preprocessing.
 
   \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}} declares (or with option ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as rewrite rules to any
   result of an evaluation.
 
+  \item \hyperlink{attribute.HOL.code-unfold-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold{\isaliteral{5F}{\isacharunderscore}}post}}} declares equations which are
+  applied as rewrite rules to any code equation during preprocessing,
+  and symmetrically to any result of an evaluation.
+  
   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code
   generator preprocessor.
 
--- a/src/HOL/Divides.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -131,7 +131,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp
--- a/src/HOL/HOL.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -1729,7 +1729,7 @@
   assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin
 
-lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+lemma equal: "equal = (op =)"
   by (rule ext equal_eq)+
 
 lemma equal_refl: "equal x x \<longleftrightarrow> True"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -495,7 +495,7 @@
 lemma [code_post]: "raise' (STR s) = raise s"
 unfolding raise'_def by (simp add: STR_inverse)
 
-lemma raise_raise' [code_inline]:
+lemma raise_raise' [code_unfold]:
   "raise s = raise' (STR s)"
   unfolding raise'_def by (simp add: STR_inverse)
 
--- a/src/HOL/Library/Executable_Set.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -67,7 +67,7 @@
   "{} = empty"
   by simp
 
-lemma [code_unfold, code_inline del]:
+lemma
   "empty = Set []"
   by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
 
--- a/src/HOL/Library/Extended_Real.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -1362,8 +1362,7 @@
 }
 moreover
 { assume "?lhs" hence "?rhs"
-  by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
-      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+  by (metis less_SUP_iff order_less_imp_le order_less_le_trans)
 } ultimately show ?thesis by auto
 qed
 
@@ -1382,8 +1381,7 @@
 }
 moreover
 { assume "?lhs" hence "?rhs"
-  by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
-      inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
+  by (metis INF_less_iff order_le_less order_less_le_trans)
 } ultimately show ?thesis by auto
 qed
 
--- a/src/HOL/Library/List_Prefix.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -74,7 +74,7 @@
 next
   assume "xs = ys @ [y] \<or> xs \<le> ys"
   then show "xs \<le> ys @ [y]"
-    by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
+    by (metis order_eq_iff order_trans prefixI)
 qed
 
 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"
--- a/src/HOL/Library/Mapping.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -90,7 +90,7 @@
 
 subsection {* Properties *}
 
-lemma keys_is_none_lookup [code_inline]:
+lemma keys_is_none_lookup [code_unfold]:
   "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   by (auto simp add: keys_def is_none_def)
 
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -84,7 +84,7 @@
 
 definition subtract
 where
-  [code_inline]: "subtract x y = y - x"
+  [code_unfold]: "subtract x y = y - x"
 
 setup {*
 let
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -185,8 +185,6 @@
     by (auto simp add: rtranclp_eq_rtrancl_path)
 qed
 
-declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
-
 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
 
 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
--- a/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -118,12 +118,12 @@
 
 definition undefined_cname :: cname 
   where [code del]: "undefined_cname = undefined"
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
 code_datatype Object Xcpt Cname undefined_cname
 
 definition undefined_val :: val
   where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
 code_datatype Unit Null Bool Intg Addr undefined_val
 
 definition E where 
--- a/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -13,18 +13,18 @@
 *}
 
 definition ObjectC :: "'c cdecl" where
-  [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
+  [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))"
 
 definition NullPointerC :: "'c cdecl" where
-  [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+  [code_unfold]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
 
 definition ClassCastC :: "'c cdecl" where
-  [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+  [code_unfold]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
 
 definition OutOfMemoryC :: "'c cdecl" where
-  [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+  [code_unfold]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
 
 definition SystemClasses :: "'c cdecl list" where
-  [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+  [code_unfold]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
 
 end
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -97,7 +97,7 @@
   [inductify]
   subcls'
 .
-lemma subcls_conv_subcls' [code_inline]:
+lemma subcls_conv_subcls' [code_unfold]:
   "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
 by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
 
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -125,11 +125,11 @@
 definition undefined_cname :: cname 
   where [code del]: "undefined_cname = undefined"
 code_datatype Object Xcpt Cname undefined_cname
-declare undefined_cname_def[symmetric, code_inline]
+declare undefined_cname_def[symmetric, code_unfold]
 
 definition undefined_val :: val
   where [code del]: "undefined_val = undefined"
-declare undefined_val_def[symmetric, code_inline]
+declare undefined_val_def[symmetric, code_unfold]
 code_datatype Unit Null Bool Intg Addr undefined_val
 
 definition
--- a/src/HOL/Nat.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Nat.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -1301,7 +1301,7 @@
 
 end
 
-declare of_nat_code [code, code_unfold, code_inline del]
+declare of_nat_code [code]
 
 text{*Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
--- a/src/HOL/Orderings.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -305,13 +305,13 @@
 
 text {* Explicit dictionaries for code generation *}
 
-lemma min_ord_min [code, code_unfold, code_inline del]:
+lemma min_ord_min [code]:
   "min = ord.min (op \<le>)"
   by (rule ext)+ (simp add: min_def ord.min_def)
 
 declare ord.min_def [code]
 
-lemma max_ord_max [code, code_unfold, code_inline del]:
+lemma max_ord_max [code]:
   "max = ord.max (op \<le>)"
   by (rule ext)+ (simp add: max_def ord.max_def)
 
--- a/src/HOL/Power.thy	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Power.thy	Fri Oct 21 16:21:12 2011 +0200
@@ -460,7 +460,7 @@
 
 subsection {* Code generator tweak *}
 
-lemma power_power_power [code, code_unfold, code_inline del]:
+lemma power_power_power [code]:
   "power = power.power (1::'a::{power}) (op *)"
   unfolding power_def power.power_def ..
 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Oct 21 16:21:12 2011 +0200
@@ -247,36 +247,37 @@
   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
 
-val dummy_phi = AAtom (ATerm ("", []))
-
-fun skip_formula ss =
+val skip_term =
   let
-    fun skip _ [] = []
-      | skip 0 (ss as "," :: _) = ss
-      | skip 0 (ss as ")" :: _) = ss
-      | skip 0 (ss as "]" :: _) = ss
-      | skip n ("(" :: ss) = skip (n + 1) ss
-      | skip n ("[" :: ss) = skip (n + 1) ss
-      | skip n ("]" :: ss) = skip (n - 1) ss
-      | skip n (")" :: ss) = skip (n - 1) ss
-      | skip n (_ :: ss) = skip n ss
-  in (dummy_phi, skip 0 ss) end
+    fun skip _ accum [] = (accum, [])
+      | skip 0 accum (ss as "," :: _) = (accum, ss)
+      | skip 0 accum (ss as ")" :: _) = (accum, ss)
+      | skip 0 accum (ss as "]" :: _) = (accum, ss)
+      | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss
+      | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss
+      | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss
+      | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss
+      | skip n accum (s :: ss) = skip n (s :: accum) ss
+  in skip 0 [] #>> (rev #> implode) end
 
 datatype source =
   File_Source of string * string option |
   Inference_Source of string * string list
 
-fun parse_dependencies x =
-  (scan_general_id ::: Scan.repeat ($$ "," |-- scan_general_id)) x
+val dummy_phi = AAtom (ATerm ("", []))
+val dummy_inference = Inference_Source ("", [])
+
+fun parse_dependencies x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x
 
 fun parse_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id --
      Scan.option ($$ "," |-- scan_general_id) --| $$ ")"
      >> File_Source
    || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
-        --| skip_formula --| $$ "," --| skip_formula --| $$ "," --| $$ "["
+        --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
         -- parse_dependencies --| $$ "]" --| $$ ")"
-       >> Inference_Source) x
+       >> Inference_Source
+   || skip_term >> K dummy_inference) x
 
 fun list_app (f, args) =
   fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
@@ -345,9 +346,8 @@
           AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
 
 val parse_tstp_extra_arguments =
-  Scan.optional ($$ "," |-- parse_source
-                 --| Scan.option ($$ "," |-- skip_formula))
-                (Inference_Source ("", []))
+  Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
+                dummy_inference
 
 val waldmeister_conjecture = "conjecture_1"
 
@@ -399,8 +399,8 @@
   ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
     || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(")
     |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
-    -- (parse_formula || skip_formula) -- parse_tstp_extra_arguments --| $$ ")"
-    --| $$ "."
+    -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
+    --| $$ ")" --| $$ "."
    >> (fn (((num, role), phi), deps) =>
           let
             val (name, rule, deps) =
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 16:21:12 2011 +0200
@@ -344,7 +344,8 @@
    required_execs = [],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
      "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --proof tptp --output_axiom_names on \
+     " --proof tptp --output_axiom_names on\
+     \ --forced_options propositional_to_bdd=off\
      \ --thanks \"Andrei and Krystof\" --input_file"
      |> sos = sosN ? prefix "--sos on ",
    proof_delims =
--- a/src/Tools/Code/code_preproc.ML	Fri Oct 21 11:27:21 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Oct 21 16:21:12 2011 +0200
@@ -518,8 +518,6 @@
   in
     Attrib.setup @{binding code_unfold} (add_del_attribute_parser add_unfold del_unfold)
         "preprocessing equations for code generator"
-    #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
-        "preprocessing equations for code generator"
     #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
         "postprocessing equations for code generator"
     #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))