clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
authorwenzelm
Wed Oct 31 15:53:32 2018 +0100 (6 months ago)
changeset 692161a52baa70aed
parent 69215 ab94035ba6ea
child 69217 a8c707352ccc
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
NEWS
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Eisbach/Tests.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Hoare_Parallel/OG_Syntax.thy
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Code_Lazy.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Set.thy
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/Tools/ghc.ML
     1.1 --- a/NEWS	Wed Oct 31 15:50:45 2018 +0100
     1.2 +++ b/NEWS	Wed Oct 31 15:53:32 2018 +0100
     1.3 @@ -15,6 +15,10 @@
     1.4  * Infix operators that begin or end with a "*" can now be paranthesized
     1.5  without additional spaces, eg "(*)" instead of "( * )".
     1.6  
     1.7 +* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation')
     1.8 +need to provide a closed expression -- without trailing semicolon. Minor
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** Isabelle/jEdit Prover IDE ***
    1.13  
     2.1 --- a/src/HOL/Deriv.thy	Wed Oct 31 15:50:45 2018 +0100
     2.2 +++ b/src/HOL/Deriv.thy	Wed Oct 31 15:53:32 2018 +0100
     2.3 @@ -62,7 +62,7 @@
     2.4          fn context =>
     2.5            Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros}
     2.6            |> map_filter eq_rule)
     2.7 -  end;
     2.8 +  end
     2.9  \<close>
    2.10  
    2.11  text \<open>
     3.1 --- a/src/HOL/Divides.thy	Wed Oct 31 15:50:45 2018 +0100
     3.2 +++ b/src/HOL/Divides.thy	Wed Oct 31 15:53:32 2018 +0100
     3.3 @@ -1278,7 +1278,7 @@
     3.4        fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
     3.5          (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
     3.6      in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
     3.7 -  end;
     3.8 +  end
     3.9  \<close>
    3.10  
    3.11  
     4.1 --- a/src/HOL/Eisbach/Tests.thy	Wed Oct 31 15:50:45 2018 +0100
     4.2 +++ b/src/HOL/Eisbach/Tests.thy	Wed Oct 31 15:53:32 2018 +0100
     4.3 @@ -530,7 +530,7 @@
     4.4    Args.term -- Args.term --
     4.5    (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
     4.6      (fn ((x, y), r) => fn ctxt =>
     4.7 -      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
     4.8 +      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt)
     4.9  \<close>
    4.10  
    4.11  lemma
     5.1 --- a/src/HOL/Groups.thy	Wed Oct 31 15:50:45 2018 +0100
     5.2 +++ b/src/HOL/Groups.thy	Wed Oct 31 15:53:32 2018 +0100
     5.3 @@ -182,7 +182,7 @@
     5.4          Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
     5.5            Syntax_Phases.term_of_typ ctxt T
     5.6        else raise Match);
     5.7 -  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
     5.8 +  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end
     5.9  \<close> \<comment> \<open>show types that are presumably too general\<close>
    5.10  
    5.11  class plus =
     6.1 --- a/src/HOL/HOL.thy	Wed Oct 31 15:50:45 2018 +0100
     6.2 +++ b/src/HOL/HOL.thy	Wed Oct 31 15:53:32 2018 +0100
     6.3 @@ -1231,7 +1231,7 @@
     6.4              SOME thm => SOME (thm RS neq_to_EQ_False)
     6.5            | NONE => NONE)
     6.6         | _ => NONE);
     6.7 -  in proc end;
     6.8 +  in proc end
     6.9  \<close>
    6.10  
    6.11  simproc_setup let_simp ("Let x f") = \<open>
     7.1 --- a/src/HOL/HOLCF/Cfun.thy	Wed Oct 31 15:50:45 2018 +0100
     7.2 +++ b/src/HOL/HOLCF/Cfun.thy	Wed Oct 31 15:53:32 2018 +0100
     7.3 @@ -35,7 +35,7 @@
     7.4  
     7.5  parse_translation \<open>
     7.6  (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
     7.7 -  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
     7.8 +  [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})]
     7.9  \<close>
    7.10  
    7.11  print_translation \<open>
    7.12 @@ -60,7 +60,7 @@
    7.13            Ast.fold_ast_p @{syntax_const "_cabs"}
    7.14              (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
    7.15        | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
    7.16 -  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
    7.17 +  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end
    7.18  \<close>
    7.19  
    7.20  print_ast_translation \<open>
     8.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:50:45 2018 +0100
     8.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:53:32 2018 +0100
     8.3 @@ -132,7 +132,7 @@
     8.4  (* rewrite (_pat x) => (succeed) *)
     8.5  (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
     8.6   [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
     8.7 -  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
     8.8 +  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})]
     8.9  \<close>
    8.10  
    8.11  text \<open>Printing Case expressions\<close>
    8.12 @@ -164,7 +164,7 @@
    8.13                (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
    8.14            end;
    8.15  
    8.16 -  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
    8.17 +  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end
    8.18  \<close>
    8.19  
    8.20  translations
     9.1 --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Wed Oct 31 15:50:45 2018 +0100
     9.2 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Wed Oct 31 15:53:32 2018 +0100
     9.3 @@ -122,7 +122,7 @@
     9.4      (@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
     9.5      (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
     9.6      (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
     9.7 -  end;
     9.8 +  end
     9.9  \<close>
    9.10  
    9.11  end
    10.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Oct 31 15:50:45 2018 +0100
    10.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Oct 31 15:53:32 2018 +0100
    10.3 @@ -110,7 +110,7 @@
    10.4  
    10.5    Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc)
    10.6  
    10.7 -end;
    10.8 +end
    10.9  \<close>
   10.10  
   10.11  end
    11.1 --- a/src/HOL/Library/Code_Lazy.thy	Wed Oct 31 15:50:45 2018 +0100
    11.2 +++ b/src/HOL/Library/Code_Lazy.thy	Wed Oct 31 15:53:32 2018 +0100
    11.3 @@ -245,7 +245,7 @@
    11.4  ML_file "code_lazy.ML"
    11.5  
    11.6  setup \<open>
    11.7 -  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs);
    11.8 +  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
    11.9  \<close>
   11.10  
   11.11  end
    12.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Oct 31 15:50:45 2018 +0100
    12.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Oct 31 15:53:32 2018 +0100
    12.3 @@ -491,7 +491,7 @@
    12.4      fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
    12.5        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    12.6  
    12.7 -  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
    12.8 +  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end
    12.9  \<close>
   12.10  
   12.11  print_translation \<open>
   12.12 @@ -517,7 +517,7 @@
   12.13    in
   12.14     [(@{type_syntax bit0}, K (bit_tr' 0)),
   12.15      (@{type_syntax bit1}, K (bit_tr' 1))]
   12.16 -  end;
   12.17 +  end
   12.18  \<close>
   12.19  
   12.20  subsection \<open>Examples\<close>
    13.1 --- a/src/HOL/Set.thy	Wed Oct 31 15:50:45 2018 +0100
    13.2 +++ b/src/HOL/Set.thy	Wed Oct 31 15:53:32 2018 +0100
    13.3 @@ -287,7 +287,7 @@
    13.4          val exP = ex_tr ctxt [idts, P];
    13.5        in Syntax.const @{const_syntax Collect} $ absdummy dummyT exP end;
    13.6  
    13.7 -  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
    13.8 +  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end
    13.9  \<close>
   13.10  
   13.11  print_translation \<open>
   13.12 @@ -326,7 +326,7 @@
   13.13            | _ => M
   13.14          end
   13.15      end;
   13.16 -  in [(@{const_syntax Collect}, setcompr_tr')] end;
   13.17 +  in [(@{const_syntax Collect}, setcompr_tr')] end
   13.18  \<close>
   13.19  
   13.20  simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
    14.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Oct 31 15:50:45 2018 +0100
    14.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Oct 31 15:53:32 2018 +0100
    14.3 @@ -175,12 +175,12 @@
    14.4  
    14.5    fun ml_tactic source ctxt =
    14.6      let
    14.7 -      val ctxt' = ctxt |> Context.proof_map
    14.8 -        (ML_Context.expression ("tactic", Position.thread_data ()) "Proof.context -> tactic"
    14.9 -          "Context.map_proof (ML_Tactic.set tactic)"
   14.10 -          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
   14.11 +      val ctxt' = ctxt
   14.12 +        |> Context.proof_map (ML_Context.expression (Input.pos_of source)
   14.13 +          (ML_Lex.read "Theory.local_setup (ML_Tactic.set (fn ctxt: Proof.context => (" @
   14.14 +           ML_Lex.read_source source @ ML_Lex.read ")))"));
   14.15      in Data.get ctxt' ctxt end;
   14.16 -end;
   14.17 +end
   14.18  \<close>
   14.19  
   14.20  
    15.1 --- a/src/Pure/Isar/attrib.ML	Wed Oct 31 15:50:45 2018 +0100
    15.2 +++ b/src/Pure/Isar/attrib.ML	Wed Oct 31 15:53:32 2018 +0100
    15.3 @@ -214,12 +214,11 @@
    15.4  fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
    15.5  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
    15.6  
    15.7 -fun attribute_setup (name, pos) source comment =
    15.8 -  ML_Lex.read_source source
    15.9 -  |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
   15.10 -    ("Context.map_proof (Attrib.local_setup " ^
   15.11 -      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
   15.12 -      " parser " ^ ML_Syntax.print_string comment ^ ")")
   15.13 +fun attribute_setup binding source comment =
   15.14 +  ML_Context.expression (Input.pos_of source)
   15.15 +    (ML_Lex.read
   15.16 +      ("Theory.local_setup (Attrib.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @
   15.17 +     ML_Lex.read_source source @ ML_Lex.read (") " ^ ML_Syntax.print_string comment ^ ")"))
   15.18    |> Context.proof_map;
   15.19  
   15.20  
    16.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 31 15:50:45 2018 +0100
    16.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 31 15:53:32 2018 +0100
    16.3 @@ -51,53 +51,46 @@
    16.4  (* generic setup *)
    16.5  
    16.6  fun setup source =
    16.7 -  ML_Lex.read_source source
    16.8 -  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
    16.9 -    "Context.map_theory setup"
   16.10 +  ML_Context.expression (Input.pos_of source)
   16.11 +    (ML_Lex.read "Theory.setup (" @ ML_Lex.read_source source @ ML_Lex.read ")")
   16.12    |> Context.theory_map;
   16.13  
   16.14  fun local_setup source =
   16.15 -  ML_Lex.read_source source
   16.16 -  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
   16.17 -    "Context.map_proof local_setup"
   16.18 +  ML_Context.expression (Input.pos_of source)
   16.19 +    (ML_Lex.read "Theory.local_setup (" @ ML_Lex.read_source source @ ML_Lex.read ")")
   16.20    |> Context.proof_map;
   16.21  
   16.22  
   16.23  (* translation functions *)
   16.24  
   16.25  fun parse_ast_translation source =
   16.26 -  ML_Lex.read_source source
   16.27 -  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
   16.28 -    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   16.29 -    "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
   16.30 +  ML_Context.expression (Input.pos_of source)
   16.31 +    (ML_Lex.read "Theory.setup (Sign.parse_ast_translation (" @
   16.32 +      ML_Lex.read_source source @ ML_Lex.read "))")
   16.33    |> Context.theory_map;
   16.34  
   16.35  fun parse_translation source =
   16.36 -  ML_Lex.read_source source
   16.37 -  |> ML_Context.expression ("parse_translation", Position.thread_data ())
   16.38 -    "(string * (Proof.context -> term list -> term)) list"
   16.39 -    "Context.map_theory (Sign.parse_translation parse_translation)"
   16.40 +  ML_Context.expression (Input.pos_of source)
   16.41 +    (ML_Lex.read "Theory.setup (Sign.parse_translation (" @
   16.42 +      ML_Lex.read_source source @ ML_Lex.read "))")
   16.43    |> Context.theory_map;
   16.44  
   16.45  fun print_translation source =
   16.46 -  ML_Lex.read_source source
   16.47 -  |> ML_Context.expression ("print_translation", Position.thread_data ())
   16.48 -    "(string * (Proof.context -> term list -> term)) list"
   16.49 -    "Context.map_theory (Sign.print_translation print_translation)"
   16.50 +  ML_Context.expression (Input.pos_of source)
   16.51 +    (ML_Lex.read "Theory.setup (Sign.print_translation (" @
   16.52 +      ML_Lex.read_source source @ ML_Lex.read "))")
   16.53    |> Context.theory_map;
   16.54  
   16.55  fun typed_print_translation source =
   16.56 -  ML_Lex.read_source source
   16.57 -  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
   16.58 -    "(string * (Proof.context -> typ -> term list -> term)) list"
   16.59 -    "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   16.60 +  ML_Context.expression (Input.pos_of source)
   16.61 +    (ML_Lex.read "Theory.setup (Sign.typed_print_translation (" @
   16.62 +      ML_Lex.read_source source @ ML_Lex.read "))")
   16.63    |> Context.theory_map;
   16.64  
   16.65  fun print_ast_translation source =
   16.66 -  ML_Lex.read_source source
   16.67 -  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
   16.68 -    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   16.69 -    "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   16.70 +  ML_Context.expression (Input.pos_of source)
   16.71 +    (ML_Lex.read "Theory.setup (Sign.print_ast_translation (" @
   16.72 +      ML_Lex.read_source source @ ML_Lex.read "))")
   16.73    |> Context.theory_map;
   16.74  
   16.75  
   16.76 @@ -142,22 +135,22 @@
   16.77  (* declarations *)
   16.78  
   16.79  fun declaration {syntax, pervasive} source =
   16.80 -  ML_Lex.read_source source
   16.81 -  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
   16.82 -    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   16.83 -      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   16.84 +  ML_Context.expression (Input.pos_of source)
   16.85 +    (ML_Lex.read
   16.86 +      ("Theory.local_setup (Local_Theory.declaration {syntax = " ^
   16.87 +        Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^ "} (") @
   16.88 +     ML_Lex.read_source source @ ML_Lex.read "))")
   16.89    |> Context.proof_map;
   16.90  
   16.91  
   16.92  (* simprocs *)
   16.93  
   16.94  fun simproc_setup name lhss source =
   16.95 -  ML_Lex.read_source source
   16.96 -  |> ML_Context.expression ("proc", Position.thread_data ())
   16.97 -    "Morphism.morphism -> Proof.context -> cterm -> thm option"
   16.98 -    ("Context.map_proof (Simplifier.define_simproc_cmd " ^
   16.99 -      ML_Syntax.atomic (ML_Syntax.make_binding name) ^
  16.100 -      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
  16.101 +  ML_Context.expression (Input.pos_of source)
  16.102 +    (ML_Lex.read
  16.103 +      ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^
  16.104 +        ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^
  16.105 +        ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})")
  16.106    |> Context.proof_map;
  16.107  
  16.108  
    17.1 --- a/src/Pure/Isar/method.ML	Wed Oct 31 15:50:45 2018 +0100
    17.2 +++ b/src/Pure/Isar/method.ML	Wed Oct 31 15:53:32 2018 +0100
    17.3 @@ -368,13 +368,12 @@
    17.4    Scan.state :|-- (fn context =>
    17.5      Scan.lift (Args.text_declaration (fn source =>
    17.6        let
    17.7 -        val context' = context |>
    17.8 -          ML_Context.expression ("tactic", Position.thread_data ())
    17.9 -            "Morphism.morphism -> thm list -> tactic"
   17.10 -            "Method.set_tactic tactic"
   17.11 -            (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
   17.12 -             ML_Lex.read_source source);
   17.13 -        val tac = the_tactic context';
   17.14 +        val tac =
   17.15 +          context
   17.16 +          |> ML_Context.expression (Input.pos_of source)
   17.17 +              (ML_Lex.read "Context.>> (Method.set_tactic (fn morphism: Morphism.morphism => fn facts: thm list => (" @
   17.18 +               ML_Lex.read_source source @ ML_Lex.read ")))")
   17.19 +          |> the_tactic;
   17.20        in
   17.21          fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
   17.22        end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
   17.23 @@ -475,13 +474,11 @@
   17.24  fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
   17.25  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
   17.26  
   17.27 -fun method_setup (name, pos) source comment =
   17.28 -  ML_Lex.read_source source
   17.29 -  |> ML_Context.expression ("parser", pos)
   17.30 -    "(Proof.context -> Proof.method) context_parser"
   17.31 -    ("Context.map_proof (Method.local_setup " ^
   17.32 -      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
   17.33 -      " parser " ^ ML_Syntax.print_string comment ^ ")")
   17.34 +fun method_setup binding source comment =
   17.35 +  ML_Context.expression (Input.pos_of source)
   17.36 +    (ML_Lex.read
   17.37 +      ("Theory.local_setup (Method.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @
   17.38 +     ML_Lex.read_source source @ ML_Lex.read (")" ^ ML_Syntax.print_string comment ^ ")"))
   17.39    |> Context.proof_map;
   17.40  
   17.41  
    18.1 --- a/src/Pure/ML/ml_context.ML	Wed Oct 31 15:50:45 2018 +0100
    18.2 +++ b/src/Pure/ML/ml_context.ML	Wed Oct 31 15:53:32 2018 +0100
    18.3 @@ -21,8 +21,8 @@
    18.4      ML_Lex.token Antiquote.antiquote list -> unit
    18.5    val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
    18.6    val exec: (unit -> unit) -> Context.generic -> Context.generic
    18.7 -  val expression: string * Position.T -> string -> string ->
    18.8 -    ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
    18.9 +  val expression: Position.T -> ML_Lex.token Antiquote.antiquote list ->
   18.10 +    Context.generic -> Context.generic
   18.11  end
   18.12  
   18.13  structure ML_Context: ML_CONTEXT =
   18.14 @@ -214,13 +214,7 @@
   18.15      SOME context' => context'
   18.16    | NONE => error "Missing context after execution");
   18.17  
   18.18 -fun expression (name, pos) constraint body ants =
   18.19 -  exec (fn () =>
   18.20 -    eval ML_Compiler.flags pos
   18.21 -     (ML_Lex.read "Context.put_generic_context (SOME (let val " @
   18.22 -       ML_Lex.read_set_range (Position.range_of_properties (Position.properties_of pos)) name @
   18.23 -      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
   18.24 -      ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
   18.25 +fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants);
   18.26  
   18.27  end;
   18.28  
    19.1 --- a/src/Pure/Tools/ghc.ML	Wed Oct 31 15:50:45 2018 +0100
    19.2 +++ b/src/Pure/Tools/ghc.ML	Wed Oct 31 15:53:32 2018 +0100
    19.3 @@ -119,9 +119,9 @@
    19.4      (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
    19.5        (fn {context = ctxt, argument, ...} =>
    19.6          ctxt |> Context.proof_map
    19.7 -          (ML_Context.expression ("result", Position.thread_data ())
    19.8 -            "string" "Context.map_proof (GHC.set_result result)"
    19.9 -            (ML_Lex.read_source argument))
   19.10 +          (ML_Context.expression (Input.pos_of argument)
   19.11 +            (ML_Lex.read "Theory.local_setup (GHC.set_result (" @
   19.12 +             ML_Lex.read_source argument @ ML_Lex.read "))"))
   19.13          |> the_result |> print_string));
   19.14  
   19.15  end;