clarified Thy_Syntax.element;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 01 16:05:38 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 01 17:36:25 2011 +0200
@@ -249,13 +249,13 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun prepare_atom commands init (cmd, proof, proper_proof) =
+fun prepare_element commands init {head, proof, proper_proof} =
   let
-    val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
+    val (tr, proper_head) = prepare_span commands head |>> Toplevel.modify_init init;
     val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
   in
-    if proper_cmd andalso proper_proof then [(tr, proof_trs)]
-    else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
+    if proper_head andalso proper_proof then [(tr, proof_trs)]
+    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   end;
 
 fun prepare_command pos str =
@@ -278,14 +278,14 @@
     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
-    val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
-      |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
+    val elements = Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
+      |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element commands init) |> flat;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
+    val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     val present =

--- a/src/Pure/Thy/thy_syntax.ML	Fri Jul 01 16:05:38 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Jul 01 17:36:25 2011 +0200
@@ -21,8 +21,9 @@
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   val present_span: span -> Output.output
   val report_span: span -> unit
-  val atom_source: (span, 'a) Source.source ->
-    (span * span list * bool, (span, 'a) Source.source) Source.source
+  type element = {head: span, proof: span list, proper_proof: bool}
+  val element_source: (span, 'a) Source.source ->
+    (element, (span, 'a) Source.source) Source.source
 end;
 
 structure Thy_Syntax: THY_SYNTAX =
@@ -159,7 +160,13 @@
 
 
 
-(** specification atoms: commands with optional proof **)
+(** specification elements: commands with optional proof **)
+
+type element = {head: span, proof: span list, proper_proof: bool};
+
+fun make_element head proof proper_proof =
+  {head = head, proof = proof, proper_proof = proper_proof};
+
 
 (* scanning spans *)
 
@@ -173,7 +180,7 @@
 val stopper = Scan.stopper (K eof) is_eof;
 
 
-(* atom_source *)
+(* element_source *)
 
 local
 
@@ -187,13 +194,14 @@
     (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
     Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
 
-val atom =
-  command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
-  Scan.one not_eof >> (fn a => (a, [], true));
+val element =
+  command_with Keyword.is_theory_goal -- proof
+    >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
+  Scan.one not_eof >> (fn a => make_element a [] true);
 
 in
 
-fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
+fun element_source src = Source.source stopper (Scan.bulk element) NONE src;
 
 end;