src/Tools/Code/code_printer.ML

   type itype = Code_Thingol.itype
   type iterm = Code_Thingol.iterm
   type const = Code_Thingol.const
   type dict = Code_Thingol.dict
 
-  val eqn_error: thm -> string -> 'a
+  val eqn_error: thm option -> string -> 'a
 
   val @@ : 'a * 'a -> 'a list
   val @| : 'a list * 'a -> 'a list
   val str: string -> Pretty.T
   val concat: Pretty.T list -> Pretty.T

     -> (int * ((fixity -> 'b -> Pretty.T)
     -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
   val simple_const_syntax: simple_const_syntax -> proto_const_syntax
   val activate_const_syntax: theory -> literals
     -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
-  val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
-    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
+  val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
+    -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
-    -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> thm -> fixity
+    -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
+  val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
+    -> thm option -> fixity
     -> iterm -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
   val dest_name: string -> string * string

 structure Code_Printer : CODE_PRINTER =
 struct
 
 open Code_Thingol;
 
-fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
+fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
+  | eqn_error NONE s = error s;
 
 (** assembling and printing text pieces **)
 
 infixr 5 @@;
 infixr 5 @|;

 
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
 type proto_const_syntax = int * (string list * (literals -> string list
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
-    -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
+    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
 type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
 fun simple_const_syntax syn =
   apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
 
 fun activate_const_syntax thy literals (n, (cs, f)) naming =