src/Pure/Isar/toplevel.ML
changeset 68839 d8251a61cce8
parent 68772 23a5e7fba837
child 68869 3739acbc2178
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 07:50:28 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:44:28 2018 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    val reset_proof: state -> state option
     1.5    type result
     1.6    val join_results: result -> (transition * state) list
     1.7 -  val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state
     1.8 +  val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
     1.9  end;
    1.10  
    1.11  structure Toplevel: TOPLEVEL =
    1.12 @@ -669,7 +669,7 @@
    1.13  val put_result = Proof.map_context o Result.put;
    1.14  
    1.15  fun timing_estimate elem =
    1.16 -  let val trs = tl (Thy_Syntax.flat_element elem)
    1.17 +  let val trs = tl (Thy_Element.flat_element elem)
    1.18    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
    1.19  
    1.20  fun future_proofs_enabled estimate st =
    1.21 @@ -693,8 +693,8 @@
    1.22  
    1.23  in
    1.24  
    1.25 -fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st
    1.26 -  | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    1.27 +fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
    1.28 +  | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
    1.29        let
    1.30          val (head_result, st') = atom_result keywords head_tr st;
    1.31          val (body_elems, end_tr) = element_rest;
    1.32 @@ -703,7 +703,7 @@
    1.33          if not (future_proofs_enabled estimate st')
    1.34          then
    1.35            let
    1.36 -            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    1.37 +            val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr];
    1.38              val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
    1.39            in (Result_List (head_result :: proof_results), st'') end
    1.40          else