src/Pure/Isar/toplevel.ML
changeset 60099 d20ca79d50e4
parent 60096 96a4765ba7d1
child 60189 0d3a62127057
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:11:04 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:22:44 2015 +0200
     1.3 @@ -72,8 +72,6 @@
     1.4    val skip_proof: (int -> int) -> transition -> transition
     1.5    val skip_proof_to_theory: (int -> bool) -> transition -> transition
     1.6    val exec_id: Document_ID.exec -> transition -> transition
     1.7 -  val unknown_theory: transition -> transition
     1.8 -  val unknown_context: transition -> transition
     1.9    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    1.10    val add_hook: (transition -> state -> state -> unit) -> unit
    1.11    val get_timing: transition -> Time.time option
    1.12 @@ -355,9 +353,6 @@
    1.13  fun malformed pos msg =
    1.14    empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    1.15  
    1.16 -val unknown_theory = imperative (fn () => warning "Unknown theory context");
    1.17 -val unknown_context = imperative (fn () => warning "Unknown context");
    1.18 -
    1.19  
    1.20  (* theory transitions *)
    1.21