tuned signature;

--- a/src/HOL/Statespace/state_space.ML	Wed Aug 08 22:14:39 2012 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Aug 09 12:39:05 2012 +0200
@@ -42,7 +42,7 @@
   val distinct_simproc : Simplifier.simproc
 
 
-  val get_comp : Context.generic -> string -> (typ * string) Option.option
+  val get_comp : Context.generic -> string -> (typ * string) option
   val get_silent : Context.generic -> bool
   val set_silent : bool -> Context.generic -> Context.generic
 

--- a/src/Pure/Isar/token.ML	Wed Aug 08 22:14:39 2012 +0200
+++ b/src/Pure/Isar/token.ML	Thu Aug 09 12:39:05 2012 +0200
@@ -53,9 +53,9 @@
   val closure: T -> T
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
-  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
-  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a