# HG changeset patch
# User haftmann
# Date 1236009519 -3600
# Node ID 2775062fd3a9624dddba06dd2f821dc32c60ad6a
# Parent  39fefb3eedfc08dd9fb6e7be80a32727ace254a0
reduced confusion code_funcgr vs. code_wellsorted

diff -r 39fefb3eedfc -r 2775062fd3a9 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Mar 02 16:58:39 2009 +0100
+++ b/doc-src/more_antiquote.ML	Mon Mar 02 16:58:39 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Doc/more_antiquote.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 More antiquotations.
@@ -92,9 +91,9 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code_Unit.check_const thy raw_const;
-    val (_, funcgr) = Code_Funcgr.make thy [const];
+    val (_, funcgr) = Code_Wellsorted.make thy [const];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
-    val thms = Code_Funcgr.eqns funcgr const
+    val thms = Code_Wellsorted.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
   in ThyOutput.output_list pretty_thm src ctxt thms end;
diff -r 39fefb3eedfc -r 2775062fd3a9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 02 16:58:39 2009 +0100
+++ b/src/HOL/HOL.thy	Mon Mar 02 16:58:39 2009 +0100
@@ -29,8 +29,8 @@
   ("~~/src/Tools/induct_tacs.ML")
   "~~/src/Tools/value.ML"
   "~~/src/Tools/code/code_name.ML"
-  "~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *)
-  (*"~~/src/Tools/code/code_funcgr.ML"*)
+  "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
+  "~~/src/Tools/code/code_wellsorted.ML" 
   "~~/src/Tools/code/code_thingol.ML"
   "~~/src/Tools/code/code_printer.ML"
   "~~/src/Tools/code/code_target.ML"
diff -r 39fefb3eedfc -r 2775062fd3a9 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Mon Mar 02 16:58:39 2009 +0100
+++ b/src/Tools/code/code_funcgr.ML	Mon Mar 02 16:58:39 2009 +0100
@@ -3,9 +3,11 @@
 
 Retrieving, normalizing and structuring code equations in graph
 with explicit dependencies.
+
+Legacy.  To be replaced by Tools/code/code_wellsorted.ML
 *)
 
-signature CODE_FUNCGR =
+signature CODE_WELLSORTED =
 sig
   type T
   val eqns: T -> string -> (thm * bool) list
@@ -21,7 +23,7 @@
   val timing: bool ref
 end
 
-structure Code_Funcgr : CODE_FUNCGR =
+structure Code_Wellsorted : CODE_WELLSORTED =
 struct
 
 (** the graph type **)
diff -r 39fefb3eedfc -r 2775062fd3a9 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
+++ b/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
@@ -597,7 +597,7 @@
      of SOME tyco => stmt_datatypecons tyco
       | NONE => (case AxClass.class_of_param thy c
          of SOME class => stmt_classparam class
-          | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
+          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
   in ensure_stmt lookup_const (declare_const thy) stmt_const c end
 and translate_term thy algbr funcgr thm (Const (c, ty)) =
       translate_app thy algbr funcgr thm ((c, ty), [])
@@ -622,7 +622,7 @@
 and translate_const thy algbr funcgr thm (c, ty) =
   let
     val tys = Sign.const_typargs thy (c, ty);
-    val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
+    val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
     val tys_args = (fst o Term.strip_type) ty;
   in
     ensure_const thy algbr funcgr c
@@ -735,7 +735,7 @@
     fun generate_consts thy algebra funcgr =
       fold_map (ensure_const thy algebra funcgr);
   in
-    invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
+    invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
     |-> project_consts
   end;
 
@@ -778,8 +778,8 @@
       in evaluator'' naming program vs_ty_t deps end;
   in (t', evaluator') end
 
-fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
-fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
+fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
+fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
 
 end; (*struct*)
 
diff -r 39fefb3eedfc -r 2775062fd3a9 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
@@ -5,7 +5,7 @@
 with explicit dependencies -- the Waisenhaus algorithm.
 *)
 
-signature CODE_FUNCGR =
+signature CODE_WELLSORTED =
 sig
   type T
   val eqns: T -> string -> (thm * bool) list
@@ -20,7 +20,7 @@
     -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
 end
 
-structure Code_Funcgr : CODE_FUNCGR =
+structure Code_Wellsorted : CODE_WELLSORTED =
 struct
 
 (** the equation graph type **)