# HG changeset patch
# User haftmann
# Date 1266573982 -3600
# Node ID ac2cab4583f4a97ed5ab26e054a513380d6e6f18
# Parent  d67857e3a8c092602e68169cf96aa16dc13a420d
context theorem is optional

diff -r d67857e3a8c0 -r ac2cab4583f4 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_eval.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -53,7 +53,7 @@
         val value_name = "Value.VALUE.value"
         val program' = program
           |> Graph.new_node (value_name,
-              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
           |> fold (curry Graph.add_edge value_name) deps;
         val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
           (the_default target some_target) "" naming program' [value_name];
diff -r d67857e3a8c0 -r ac2cab4583f4 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -50,71 +50,71 @@
       Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
     fun print_typscheme tyvars (vs, ty) =
       Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
-    fun print_term tyvars thm vars fxy (IConst c) =
-          print_app tyvars thm vars fxy (c, [])
-      | print_term tyvars thm vars fxy (t as (t1 `$ t2)) =
+    fun print_term tyvars some_thm vars fxy (IConst c) =
+          print_app tyvars some_thm vars fxy (c, [])
+      | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
           (case Code_Thingol.unfold_const_app t
-           of SOME app => print_app tyvars thm vars fxy app
+           of SOME app => print_app tyvars some_thm vars fxy app
             | _ =>
                 brackify fxy [
-                  print_term tyvars thm vars NOBR t1,
-                  print_term tyvars thm vars BR t2
+                  print_term tyvars some_thm vars NOBR t1,
+                  print_term tyvars some_thm vars BR t2
                 ])
-      | print_term tyvars thm vars fxy (IVar NONE) =
+      | print_term tyvars some_thm vars fxy (IVar NONE) =
           str "_"
-      | print_term tyvars thm vars fxy (IVar (SOME v)) =
+      | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
           (str o lookup_var vars) v
-      | print_term tyvars thm vars fxy (t as _ `|=> _) =
+      | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            val (ps, vars') = fold_map (print_bind tyvars thm BR o fst) binds vars;
-          in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars thm vars' NOBR t') end
-      | print_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
+            val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
+          in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
+      | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then print_case tyvars thm vars fxy cases
-                else print_app tyvars thm vars fxy c_ts
-            | NONE => print_case tyvars thm vars fxy cases)
-    and print_app_expr tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
-     of [] => (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
+                then print_case tyvars some_thm vars fxy cases
+                else print_app tyvars some_thm vars fxy c_ts
+            | NONE => print_case tyvars some_thm vars fxy cases)
+    and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+     of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
       | fingerprint => let
           val ts_fingerprint = ts ~~ take (length ts) fingerprint;
           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
             (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
-          fun print_term_anno (t, NONE) _ = print_term tyvars thm vars BR t
+          fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
             | print_term_anno (t, SOME _) ty =
-                brackets [print_term tyvars thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
+                brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
         in
           if needs_annotation then
             (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
-          else (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
+          else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
         end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
-    and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars) thm fxy p
-    and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
+    and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
+    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun print_match ((pat, ty), t) vars =
               vars
-              |> print_bind tyvars thm BR pat
-              |>> (fn p => semicolon [p, str "=", print_term tyvars thm vars NOBR t])
+              |> print_bind tyvars some_thm BR pat
+              |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
             val (ps, vars') = fold_map print_match binds vars;
           in brackify_block fxy (str "let {")
             ps
-            (concat [str "}", str "in", print_term tyvars thm vars' NOBR body])
+            (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
           end
-      | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
+      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let
             fun print_select (pat, body) =
               let
-                val (p, vars') = print_bind tyvars thm NOBR pat vars;
-              in semicolon [p, str "->", print_term tyvars thm vars' NOBR body] end;
+                val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
+              in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
           in brackify_block fxy
-            (concat [str "case", print_term tyvars thm vars NOBR t, str "of", str "{"])
+            (concat [str "case", print_term tyvars some_thm vars NOBR t, str "of", str "{"])
             (map print_select clauses)
             (str "}") 
           end
-      | print_case tyvars thm vars fxy ((_, []), _) =
+      | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
     fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
           let
@@ -128,7 +128,7 @@
                 @@ (str o ML_Syntax.print_string
                     o Long_Name.base_name o Long_Name.qualifier) name
               );
-            fun print_eqn ((ts, t), (thm, _)) =
+            fun print_eqn ((ts, t), (some_thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
@@ -139,9 +139,9 @@
               in
                 semicolon (
                   (str o deresolve_base) name
-                  :: map (print_term tyvars thm vars BR) ts
+                  :: map (print_term tyvars some_thm vars BR) ts
                   @ str "="
-                  @@ print_term tyvars thm vars NOBR t
+                  @@ print_term tyvars some_thm vars NOBR t
                 )
               end;
           in
@@ -222,7 +222,7 @@
              of NONE => semicolon [
                     (str o deresolve_base) classparam,
                     str "=",
-                    print_app tyvars thm reserved NOBR (c_inst, [])
+                    print_app tyvars (SOME thm) reserved NOBR (c_inst, [])
                   ]
               | SOME (k, pr) =>
                   let
@@ -238,9 +238,9 @@
                       (*dictionaries are not relevant at this late stage*)
                   in
                     semicolon [
-                      print_term tyvars thm vars NOBR lhs,
+                      print_term tyvars (SOME thm) vars NOBR lhs,
                       str "=",
-                      print_term tyvars thm vars NOBR rhs
+                      print_term tyvars (SOME thm) vars NOBR rhs
                     ]
                   end;
           in
diff -r d67857e3a8c0 -r ac2cab4583f4 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -28,7 +28,7 @@
 val target_OCaml = "OCaml";
 
 datatype ml_binding =
-    ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+    ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
   | ML_Instance of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * ((string * const) * (thm * bool)) list));
@@ -94,79 +94,79 @@
     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
-    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
-          print_app is_pseudo_fun thm vars fxy (c, [])
-      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
+    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
+          print_app is_pseudo_fun some_thm vars fxy (c, [])
+      | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
           str "_"
-      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
+      | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
-      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
+      | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
-            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
-                print_term is_pseudo_fun thm vars BR t2])
-      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
+           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+            | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
+                print_term is_pseudo_fun some_thm vars BR t2])
+      | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             fun print_abs (pat, ty) =
-              print_bind is_pseudo_fun thm NOBR pat
+              print_bind is_pseudo_fun some_thm NOBR pat
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map print_abs binds vars;
-          in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
-      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
+          in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
+      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then print_case is_pseudo_fun thm vars fxy cases
-                else print_app is_pseudo_fun thm vars fxy c_ts
-            | NONE => print_case is_pseudo_fun thm vars fxy cases)
-    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
+                then print_case is_pseudo_fun some_thm vars fxy cases
+                else print_app is_pseudo_fun some_thm vars fxy c_ts
+            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         let val k = length tys in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
-            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
-          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
+            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
         end
       else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
-        @ map (print_term is_pseudo_fun thm vars BR) ts
-    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
-      (print_term is_pseudo_fun) syntax_const thm vars
+        @ map (print_term is_pseudo_fun some_thm vars BR) ts
+    and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
+      (print_term is_pseudo_fun) syntax_const some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
-    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun print_match ((pat, ty), t) vars =
               vars
-              |> print_bind is_pseudo_fun thm NOBR pat
+              |> print_bind is_pseudo_fun some_thm NOBR pat
               |>> (fn p => semicolon [str "val", p, str "=",
-                    print_term is_pseudo_fun thm vars NOBR t])
+                    print_term is_pseudo_fun some_thm vars NOBR t])
             val (ps, vars') = fold_map print_match binds vars;
           in
             Pretty.chunks [
               Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
-              Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
+              Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
               str "end"
             ]
           end
-      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
+      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun print_select delim (pat, body) =
               let
-                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
+                val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
               in
-                concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
+                concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
               end;
           in
             brackets (
               str "case"
-              :: print_term is_pseudo_fun thm vars NOBR t
+              :: print_term is_pseudo_fun some_thm vars NOBR t
               :: print_select "of" clause
               :: map (print_select "|") clauses
             )
           end
-      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
+      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
           (concat o map str) ["raise", "Fail", "\"empty case\""];
     fun print_val_decl print_typscheme (name, typscheme) = concat
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
@@ -186,7 +186,7 @@
     fun print_def is_pseudo_fun needs_typ definer
           (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
           let
-            fun print_eqn definer ((ts, t), (thm, _)) =
+            fun print_eqn definer ((ts, t), (some_thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
@@ -202,9 +202,9 @@
                   prolog
                   :: (if is_pseudo_fun name then [str "()"]
                       else print_dict_args vs
-                        @ map (print_term is_pseudo_fun thm vars BR) ts)
+                        @ map (print_term is_pseudo_fun some_thm vars BR) ts)
                   @ str "="
-                  @@ print_term is_pseudo_fun thm vars NOBR t
+                  @@ print_term is_pseudo_fun some_thm vars NOBR t
                 )
               end
             val shift = if null eqs then I else
@@ -229,7 +229,7 @@
               concat [
                 (str o Long_Name.base_name o deresolve) classparam,
                 str "=",
-                print_app (K false) thm reserved NOBR (c_inst, [])
+                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
@@ -393,71 +393,71 @@
     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
-    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
-          print_app is_pseudo_fun thm vars fxy (c, [])
-      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
+    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
+          print_app is_pseudo_fun some_thm vars fxy (c, [])
+      | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
           str "_"
-      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
+      | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
           str (lookup_var vars v)
-      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
+      | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
-           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
-            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
-                print_term is_pseudo_fun thm vars BR t2])
-      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
+           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+            | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
+                print_term is_pseudo_fun some_thm vars BR t2])
+      | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
-            val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars;
-          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
-      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
+            val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
+          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
+      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then print_case is_pseudo_fun thm vars fxy cases
-                else print_app is_pseudo_fun thm vars fxy c_ts
-            | NONE => print_case is_pseudo_fun thm vars fxy cases)
-    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
+                then print_case is_pseudo_fun some_thm vars fxy cases
+                else print_app is_pseudo_fun some_thm vars fxy c_ts
+            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
       if is_cons c then
         let val k = length tys in
           if length ts = k
           then (str o deresolve) c
-            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
-          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
+            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
         end
       else if is_pseudo_fun c
         then (str o deresolve) c @@ str "()"
       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
-        @ map (print_term is_pseudo_fun thm vars BR) ts
-    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
-      (print_term is_pseudo_fun) syntax_const thm vars
+        @ map (print_term is_pseudo_fun some_thm vars BR) ts
+    and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
+      (print_term is_pseudo_fun) syntax_const some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
-    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
+    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun print_let ((pat, ty), t) vars =
               vars
-              |> print_bind is_pseudo_fun thm NOBR pat
+              |> print_bind is_pseudo_fun some_thm NOBR pat
               |>> (fn p => concat
-                  [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"])
+                  [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map print_let binds vars;
           in
             brackify_block fxy (Pretty.chunks ps) []
-              (print_term is_pseudo_fun thm vars' NOBR body)
+              (print_term is_pseudo_fun some_thm vars' NOBR body)
           end
-      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
+      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun print_select delim (pat, body) =
               let
-                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
-              in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
+                val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
+              in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
           in
             brackets (
               str "match"
-              :: print_term is_pseudo_fun thm vars NOBR t
+              :: print_term is_pseudo_fun some_thm vars NOBR t
               :: print_select "with" clause
               :: map (print_select "|") clauses
             )
           end
-      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
+      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
           (concat o map str) ["failwith", "\"empty case\""];
     fun print_val_decl print_typscheme (name, typscheme) = concat
       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
@@ -477,7 +477,7 @@
     fun print_def is_pseudo_fun needs_typ definer
           (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
           let
-            fun print_eqn ((ts, t), (thm, _)) =
+            fun print_eqn ((ts, t), (some_thm, _)) =
               let
                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
@@ -485,11 +485,11 @@
                       (insert (op =)) ts []);
               in concat [
                 (Pretty.block o Pretty.commas)
-                  (map (print_term is_pseudo_fun thm vars NOBR) ts),
+                  (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
                 str "->",
-                print_term is_pseudo_fun thm vars NOBR t
+                print_term is_pseudo_fun some_thm vars NOBR t
               ] end;
-            fun print_eqns is_pseudo [((ts, t), (thm, _))] =
+            fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
                   let
                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved
@@ -500,9 +500,9 @@
                   in
                     concat (
                       (if is_pseudo then [str "()"]
-                        else map (print_term is_pseudo_fun thm vars BR) ts)
+                        else map (print_term is_pseudo_fun some_thm vars BR) ts)
                       @ str "="
-                      @@ print_term is_pseudo_fun thm vars NOBR t
+                      @@ print_term is_pseudo_fun some_thm vars NOBR t
                     )
                   end
               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
@@ -562,7 +562,7 @@
               concat [
                 (str o deresolve) classparam,
                 str "=",
-                print_app (K false) thm reserved NOBR (c_inst, [])
+                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
@@ -758,8 +758,8 @@
           let
             val eqs = filter (snd o snd) raw_eqs;
             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
-               of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
-                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
+               of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
+                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
                 | _ => (eqs, NONE)
               else (eqs, NONE)
diff -r d67857e3a8c0 -r ac2cab4583f4 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -11,7 +11,7 @@
   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
@@ -78,12 +78,12 @@
   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)
@@ -96,7 +96,8 @@
 
 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 **)
 
@@ -243,9 +244,9 @@
   -> 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;
diff -r d67857e3a8c0 -r ac2cab4583f4 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -34,33 +34,33 @@
       Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
     fun print_var vars NONE = str "_"
       | print_var vars (SOME v) = (str o lookup_var vars) v
-    fun print_term tyvars is_pat thm vars fxy (IConst c) =
-          print_app tyvars is_pat thm vars fxy (c, [])
-      | print_term tyvars is_pat thm vars fxy (t as (t1 `$ t2)) =
+    fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
+          print_app tyvars is_pat some_thm vars fxy (c, [])
+      | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
           (case Code_Thingol.unfold_const_app t
-           of SOME app => print_app tyvars is_pat thm vars fxy app
+           of SOME app => print_app tyvars is_pat some_thm vars fxy app
             | _ => applify "(" ")" fxy
-                (print_term tyvars is_pat thm vars BR t1)
-                [print_term tyvars is_pat thm vars NOBR t2])
-      | print_term tyvars is_pat thm vars fxy (IVar v) =
+                (print_term tyvars is_pat some_thm vars BR t1)
+                [print_term tyvars is_pat some_thm vars NOBR t2])
+      | print_term tyvars is_pat some_thm vars fxy (IVar v) =
           print_var vars v
-      | print_term tyvars is_pat thm vars fxy ((v, ty) `|=> t) =
+      | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
           let
             val vars' = intro_vars (the_list v) vars;
           in
             concat [
               Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
               str "=>",
-              print_term tyvars false thm vars' NOBR t
+              print_term tyvars false some_thm vars' NOBR t
             ]
           end 
-      | print_term tyvars is_pat thm vars fxy (ICase (cases as (_, t0))) =
+      | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then print_case tyvars thm vars fxy cases
-                else print_app tyvars is_pat thm vars fxy c_ts
-            | NONE => print_case tyvars thm vars fxy cases)
-    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
+                then print_case tyvars some_thm vars fxy cases
+                else print_app tyvars is_pat some_thm vars fxy c_ts
+            | NONE => print_case tyvars some_thm vars fxy cases)
+    and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
       let
         val k = length ts;
         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
@@ -69,47 +69,47 @@
         val (no_syntax, print') = case syntax_const c
          of NONE => (true, fn ts => applify "(" ")" fxy
               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
-                (map (print_term tyvars is_pat thm vars NOBR) ts))
+                (map (print_term tyvars is_pat some_thm vars NOBR) ts))
           | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
+              print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
       in if k = l then print' ts
       else if k < l then
-        print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
+        print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
       else let
         val (ts1, ts23) = chop l ts;
       in
         Pretty.block (print' ts1 :: map (fn t => Pretty.block
-          [str ".apply(", print_term tyvars is_pat thm vars NOBR t, str ")"]) ts23)
+          [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
       end end
-    and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars true) thm fxy p
-    and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
+    and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
+    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun print_match ((pat, ty), t) vars =
               vars
-              |> print_bind tyvars thm BR pat
+              |> print_bind tyvars some_thm BR pat
               |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
                 str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
-                  str "=", print_term tyvars false thm vars NOBR t])
+                  str "=", print_term tyvars false some_thm vars NOBR t])
             val (ps, vars') = fold_map print_match binds vars;
           in
             brackify_block fxy
               (str "{")
-              (ps @| print_term tyvars false thm vars' NOBR body)
+              (ps @| print_term tyvars false some_thm vars' NOBR body)
               (str "}")
           end
-      | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
+      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
           let
             fun print_select (pat, body) =
               let
-                val (p, vars') = print_bind tyvars thm NOBR pat vars;
-              in concat [str "case", p, str "=>", print_term tyvars false thm vars' NOBR body] end;
+                val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
+              in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
           in brackify_block fxy
-            (concat [print_term tyvars false thm vars NOBR t, str "match", str "{"])
+            (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
             (map print_select clauses)
             (str "}") 
           end
-      | print_case tyvars thm vars fxy ((_, []), _) =
+      | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
     fun implicit_arguments tyvars vs vars =
       let
@@ -140,7 +140,7 @@
               end
           | eqs =>
               let
-                val tycos = fold (fn ((ts, t), (thm, _)) =>
+                val tycos = fold (fn ((ts, t), _) =>
                   fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
                 val tyvars = reserved
                   |> intro_base_names
@@ -164,12 +164,12 @@
                   (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
                 fun print_tuple [p] = p
                   | print_tuple ps = enum "," "(" ")" ps;
-                fun print_rhs vars' ((_, t), (thm, _)) = print_term tyvars false thm vars' NOBR t;
-                fun print_clause (eq as ((ts, _), (thm, _))) =
+                fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
+                fun print_clause (eq as ((ts, _), (some_thm, _))) =
                   let
                     val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
                   in
-                    concat [str "case", print_tuple (map (print_term tyvars true thm vars' NOBR) ts),
+                    concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
                       str "=>", print_rhs vars' eq]
                   end;
                 val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
@@ -267,7 +267,7 @@
                     auxs tys), str "=>"]];
               in 
                 concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
-                  str "="] @ args @ [print_app tyvars false thm vars NOBR (const, map (IVar o SOME) auxs)])
+                  str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
               end;
           in
             Pretty.chunks [
@@ -352,15 +352,15 @@
      of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
       | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
       | Code_Thingol.Datatypecons (_, tyco) =>
-          let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
-          in (length o the o AList.lookup (op =) dtcos) c end
+          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
+          in (length o the o AList.lookup (op =) constrs) c end
       | Code_Thingol.Classparam (_, class) =>
           let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
           in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
     fun is_singleton c = case Graph.get_node program c
      of Code_Thingol.Datatypecons (_, tyco) =>
-          let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
-          in (null o the o AList.lookup (op =) dtcos) c end
+          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
+          in (null o the o AList.lookup (op =) constrs) c end
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
       reserved args_num is_singleton deresolver;