--- a/ProgTutorial/Advanced.thy	Fri Jul 26 16:30:33 2013 +0200
+++ b/ProgTutorial/Advanced.thy	Wed Jul 31 15:44:28 2013 +0100
@@ -148,49 +148,6 @@
   the modified one @{text thy'}. Such buggy code will always result into 
   a runtime error message about stale theories.
 
-  However, sometimes it does make sense to work with two theories at the same
-  time, especially in the context of parsing and typing. In the code below we
-  use in Line 3 the function @{ML_ind copy in Theory} from the structure
-  @{ML_struct Theory} for obtaining a new theory that contains the same
-  data, but is unrelated to the existing theory.
-*}
-
-setup %graylinenos {* fn thy => 
-let
-  val tmp_thy = Theory.copy thy
-  val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn)
-  val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
-  val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
-  val trm2 = Syntax.read_term_global thy "FOO baz"
-  val _ = pwriteln 
-    (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))
-in
-  thy
-end *}
-
-text {*
-  That means we can make changes to the theory @{text tmp_thy} without
-  affecting the current theory @{text thy}. In this case we declare in @{text
-  "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code
-  is that we next, in Lines 6 and 7, parse a string to become a term (both
-  times the string is @{text [quotes] "FOO baz"}). But since we parse the string
-  once in the context of the theory @{text tmp_thy'} in which @{text FOO} is
-  declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context 
-  of @{text thy} where it is not, we obtain two different terms, namely 
-
-  \begin{isabelle}
-  \begin{graybox}
-  @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline
-  @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}
-  \end{graybox}
-  \end{isabelle}
-
-  There are two reasons for parsing a term in a temporary theory. One is to
-  obtain fully qualified names for constants and the other is appropriate type 
-  inference. This is relevant in situations where definitions are made later, 
-  but parsing and type inference has to take already proceed as if the definitions 
-  were already made.
-
   \begin{readmore}
   Most of the functions about theories are implemented in
   @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}.

Binary file progtutorial.pdf has changed