150 

   151   However, sometimes it does make sense to work with two theories at the same

   152   time, especially in the context of parsing and typing. In the code below we

   153   use in Line 3 the function @{ML_ind copy in Theory} from the structure

   154   @{ML_struct Theory} for obtaining a new theory that contains the same

   155   data, but is unrelated to the existing theory.

   156 *}

   157 

   158 setup %graylinenos {* fn thy => 

   159 let

   160   val tmp_thy = Theory.copy thy

   161   val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn)

   162   val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy

   163   val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"

   164   val trm2 = Syntax.read_term_global thy "FOO baz"

   165   val _ = pwriteln 

   166     (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))

   167 in

   168   thy

   169 end *}

   170 

   171 text {*

   172   That means we can make changes to the theory @{text tmp_thy} without

   173   affecting the current theory @{text thy}. In this case we declare in @{text

   174   "tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code

   175   is that we next, in Lines 6 and 7, parse a string to become a term (both

   176   times the string is @{text [quotes] "FOO baz"}). But since we parse the string

   177   once in the context of the theory @{text tmp_thy'} in which @{text FOO} is

   178   declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context 

   179   of @{text thy} where it is not, we obtain two different terms, namely 

   180 

   181   \begin{isabelle}

   182   \begin{graybox}

   183   @{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline

   184   @{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}

   185   \end{graybox}

   186   \end{isabelle}

   187 

   188   There are two reasons for parsing a term in a temporary theory. One is to

   189   obtain fully qualified names for constants and the other is appropriate type 

   190   inference. This is relevant in situations where definitions are made later, 

   191   but parsing and type inference has to take already proceed as if the definitions 

   192   were already made.