1.1 --- a/doc-src/more_antiquote.ML	Mon Mar 02 16:58:39 2009 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Mar 02 16:58:39 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Doc/more_antiquote.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  
     1.8  More antiquotations.
     1.9 @@ -92,9 +91,9 @@
    1.10    let
    1.11      val thy = ProofContext.theory_of ctxt;
    1.12      val const = Code_Unit.check_const thy raw_const;
    1.13 -    val (_, funcgr) = Code_Funcgr.make thy [const];
    1.14 +    val (_, funcgr) = Code_Wellsorted.make thy [const];
    1.15      fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    1.16 -    val thms = Code_Funcgr.eqns funcgr const
    1.17 +    val thms = Code_Wellsorted.eqns funcgr const
    1.18        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.19        |> map (holize o no_vars ctxt o AxClass.overload thy);
    1.20    in ThyOutput.output_list pretty_thm src ctxt thms end;

     2.1 --- a/src/HOL/HOL.thy	Mon Mar 02 16:58:39 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Mar 02 16:58:39 2009 +0100
     2.3 @@ -29,8 +29,8 @@
     2.4    ("~~/src/Tools/induct_tacs.ML")
     2.5    "~~/src/Tools/value.ML"
     2.6    "~~/src/Tools/code/code_name.ML"
     2.7 -  "~~/src/Tools/code/code_wellsorted.ML" (* formal dependency *)
     2.8 -  (*"~~/src/Tools/code/code_funcgr.ML"*)
     2.9 +  "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
    2.10 +  "~~/src/Tools/code/code_wellsorted.ML" 
    2.11    "~~/src/Tools/code/code_thingol.ML"
    2.12    "~~/src/Tools/code/code_printer.ML"
    2.13    "~~/src/Tools/code/code_target.ML"

     3.1 --- a/src/Tools/code/code_funcgr.ML	Mon Mar 02 16:58:39 2009 +0100
     3.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Mar 02 16:58:39 2009 +0100
     3.3 @@ -3,9 +3,11 @@
     3.4  
     3.5  Retrieving, normalizing and structuring code equations in graph
     3.6  with explicit dependencies.
     3.7 +
     3.8 +Legacy.  To be replaced by Tools/code/code_wellsorted.ML
     3.9  *)
    3.10  
    3.11 -signature CODE_FUNCGR =
    3.12 +signature CODE_WELLSORTED =
    3.13  sig
    3.14    type T
    3.15    val eqns: T -> string -> (thm * bool) list
    3.16 @@ -21,7 +23,7 @@
    3.17    val timing: bool ref
    3.18  end
    3.19  
    3.20 -structure Code_Funcgr : CODE_FUNCGR =
    3.21 +structure Code_Wellsorted : CODE_WELLSORTED =
    3.22  struct
    3.23  
    3.24  (** the graph type **)

     4.1 --- a/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
     4.2 +++ b/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
     4.3 @@ -597,7 +597,7 @@
     4.4       of SOME tyco => stmt_datatypecons tyco
     4.5        | NONE => (case AxClass.class_of_param thy c
     4.6           of SOME class => stmt_classparam class
     4.7 -          | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
     4.8 +          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
     4.9    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    4.10  and translate_term thy algbr funcgr thm (Const (c, ty)) =
    4.11        translate_app thy algbr funcgr thm ((c, ty), [])
    4.12 @@ -622,7 +622,7 @@
    4.13  and translate_const thy algbr funcgr thm (c, ty) =
    4.14    let
    4.15      val tys = Sign.const_typargs thy (c, ty);
    4.16 -    val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
    4.17 +    val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
    4.18      val tys_args = (fst o Term.strip_type) ty;
    4.19    in
    4.20      ensure_const thy algbr funcgr c
    4.21 @@ -735,7 +735,7 @@
    4.22      fun generate_consts thy algebra funcgr =
    4.23        fold_map (ensure_const thy algebra funcgr);
    4.24    in
    4.25 -    invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
    4.26 +    invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
    4.27      |-> project_consts
    4.28    end;
    4.29  
    4.30 @@ -778,8 +778,8 @@
    4.31        in evaluator'' naming program vs_ty_t deps end;
    4.32    in (t', evaluator') end
    4.33  
    4.34 -fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
    4.35 -fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
    4.36 +fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
    4.37 +fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
    4.38  
    4.39  end; (*struct*)
    4.40  

     5.1 --- a/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
     5.2 +++ b/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  with explicit dependencies -- the Waisenhaus algorithm.
     5.5  *)
     5.6  
     5.7 -signature CODE_FUNCGR =
     5.8 +signature CODE_WELLSORTED =
     5.9  sig
    5.10    type T
    5.11    val eqns: T -> string -> (thm * bool) list
    5.12 @@ -20,7 +20,7 @@
    5.13      -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    5.14  end
    5.15  
    5.16 -structure Code_Funcgr : CODE_FUNCGR =
    5.17 +structure Code_Wellsorted : CODE_WELLSORTED =
    5.18  struct
    5.19  
    5.20  (** the equation graph type **)