| changeset 48741 | 98e98181882d |
| parent 46961 | 5c6955f487e5 |
| child 49754 | acafcac41690 |
--- 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