1.1 --- a/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    type const = Code_Thingol.const
     1.5    type dict = Code_Thingol.dict
     1.6  
     1.7 -  val eqn_error: thm -> string -> 'a
     1.8 +  val eqn_error: thm option -> string -> 'a
     1.9  
    1.10    val @@ : 'a * 'a -> 'a list
    1.11    val @| : 'a list * 'a -> 'a list
    1.12 @@ -78,12 +78,12 @@
    1.13    val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    1.14    val activate_const_syntax: theory -> literals
    1.15      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    1.16 -  val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.17 -    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.18 +  val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.19 +    -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.20      -> (string -> const_syntax option)
    1.21 -    -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.22 -  val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.23 -    -> thm -> fixity
    1.24 +    -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    1.25 +  val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.26 +    -> thm option -> fixity
    1.27      -> iterm -> var_ctxt -> Pretty.T * var_ctxt
    1.28  
    1.29    val mk_name_module: Name.context -> string option -> (string -> string option)
    1.30 @@ -96,7 +96,8 @@
    1.31  
    1.32  open Code_Thingol;
    1.33  
    1.34 -fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
    1.35 +fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
    1.36 +  | eqn_error NONE s = error s;
    1.37  
    1.38  (** assembling and printing text pieces **)
    1.39  
    1.40 @@ -243,9 +244,9 @@
    1.41    -> fixity -> (iterm * itype) list -> Pretty.T);
    1.42  type proto_const_syntax = int * (string list * (literals -> string list
    1.43    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    1.44 -    -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    1.45 +    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    1.46  type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.47 -  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.48 +  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    1.49  
    1.50  fun simple_const_syntax syn =
    1.51    apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;