# HG changeset patch
# User haftmann
# Date 1249886257 -7200
# Node ID 5ef633275b15a096a21f35a3ec650876f627717b
# Parent  3f7984175fdd4d0f362b47216c78033eecd0ef7c
attempt to move desymbolization to translation

diff -r 3f7984175fdd -r 5ef633275b15 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Jul 31 10:49:09 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Aug 10 08:37:37 2009 +0200
@@ -150,7 +150,6 @@
     |> (map o apfst) (AxClass.unoverload thy)
     |> map (Code.assert_eqn thy)
     |> burrow_fst (same_arity thy)
-    |> burrow_fst (Code.desymbolize_all_vars thy)
   end;
 
 fun preprocess_conv thy ct =
diff -r 3f7984175fdd -r 5ef633275b15 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Jul 31 10:49:09 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Aug 10 08:37:37 2009 +0200
@@ -498,15 +498,15 @@
     fun stmt_classparam class =
       ensure_class thy algbr funcgr class
       #>> (fn class => Classparam (c, class));
-    fun stmt_fun ((vs, ty), raw_thms) =
+    fun stmt_fun ((vs, ty), raw_eqns) =
       let
-        val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
-          then raw_thms
-          else (map o apfst) (Code.expand_eta thy 1) raw_thms;
+        val eqns = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
+          then raw_eqns
+          else (map o apfst) (Code.expand_eta thy 1) raw_eqns;
       in
         fold_map (translate_tyvar_sort thy algbr funcgr) vs
         ##>> translate_typ thy algbr funcgr ty
-        ##>> fold_map (translate_eq thy algbr funcgr) thms
+        ##>> translate_eqns thy algbr funcgr eqns
         #>> (fn info => Fun (c, info))
       end;
     val stmt_const = case Code.get_datatype_of_constr thy c
@@ -597,7 +597,10 @@
             translate_term thy algbr funcgr thm t'
             ##>> fold_map (translate_term thy algbr funcgr thm) ts
             #>> (fn (t, ts) => t `$$ ts)
-and translate_eq thy algbr funcgr (thm, proper) =
+and translate_eqns thy algbr funcgr eqns =
+  fold_map (translate_eqn thy algbr funcgr)
+    (burrow_fst (Code.desymbolize_all_vars thy) eqns)
+and translate_eqn thy algbr funcgr (thm, proper) =
   let
     val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
       o Logic.unvarify o prop_of) thm;