1.1 --- a/doc-src/more_antiquote.ML	Mon Mar 02 17:26:23 2009 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Mar 02 18:50:41 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 17:26:23 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Mar 02 18:50:41 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/HOL/Tools/datatype_package.ML	Mon Mar 02 17:26:23 2009 +0100
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Mar 02 18:50:41 2009 +0100
     3.3 @@ -631,8 +631,8 @@
     3.4  
     3.5  local
     3.6  
     3.7 -val sym_datatype = Pretty.str "\\isacommand{datatype}";
     3.8 -val sym_binder = Pretty.str "\\ {\\isacharequal}";
     3.9 +val sym_datatype = Pretty.command "datatype";
    3.10 +val sym_binder = Pretty.str "\\ {\\isacharequal}"; (*FIXME use proper symbol*)
    3.11  val sym_sep = Pretty.str "{\\isacharbar}\\ ";
    3.12  
    3.13  in

     4.1 --- a/src/Tools/code/code_funcgr.ML	Mon Mar 02 17:26:23 2009 +0100
     4.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Mar 02 18:50:41 2009 +0100
     4.3 @@ -3,9 +3,11 @@
     4.4  
     4.5  Retrieving, normalizing and structuring code equations in graph
     4.6  with explicit dependencies.
     4.7 +
     4.8 +Legacy.  To be replaced by Tools/code/code_wellsorted.ML
     4.9  *)
    4.10  
    4.11 -signature CODE_FUNCGR =
    4.12 +signature CODE_WELLSORTED =
    4.13  sig
    4.14    type T
    4.15    val eqns: T -> string -> (thm * bool) list
    4.16 @@ -21,7 +23,7 @@
    4.17    val timing: bool ref
    4.18  end
    4.19  
    4.20 -structure Code_Funcgr : CODE_FUNCGR =
    4.21 +structure Code_Wellsorted : CODE_WELLSORTED =
    4.22  struct
    4.23  
    4.24  (** the graph type **)

     5.1 --- a/src/Tools/code/code_thingol.ML	Mon Mar 02 17:26:23 2009 +0100
     5.2 +++ b/src/Tools/code/code_thingol.ML	Mon Mar 02 18:50:41 2009 +0100
     5.3 @@ -597,7 +597,7 @@
     5.4       of SOME tyco => stmt_datatypecons tyco
     5.5        | NONE => (case AxClass.class_of_param thy c
     5.6           of SOME class => stmt_classparam class
     5.7 -          | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
     5.8 +          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
     5.9    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    5.10  and translate_term thy algbr funcgr thm (Const (c, ty)) =
    5.11        translate_app thy algbr funcgr thm ((c, ty), [])
    5.12 @@ -622,7 +622,7 @@
    5.13  and translate_const thy algbr funcgr thm (c, ty) =
    5.14    let
    5.15      val tys = Sign.const_typargs thy (c, ty);
    5.16 -    val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
    5.17 +    val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
    5.18      val tys_args = (fst o Term.strip_type) ty;
    5.19    in
    5.20      ensure_const thy algbr funcgr c
    5.21 @@ -735,7 +735,7 @@
    5.22      fun generate_consts thy algebra funcgr =
    5.23        fold_map (ensure_const thy algebra funcgr);
    5.24    in
    5.25 -    invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
    5.26 +    invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
    5.27      |-> project_consts
    5.28    end;
    5.29  
    5.30 @@ -778,8 +778,8 @@
    5.31        in evaluator'' naming program vs_ty_t deps end;
    5.32    in (t', evaluator') end
    5.33  
    5.34 -fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
    5.35 -fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
    5.36 +fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
    5.37 +fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
    5.38  
    5.39  end; (*struct*)
    5.40  

     6.1 --- a/src/Tools/code/code_wellsorted.ML	Mon Mar 02 17:26:23 2009 +0100
     6.2 +++ b/src/Tools/code/code_wellsorted.ML	Mon Mar 02 18:50:41 2009 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  with explicit dependencies -- the Waisenhaus algorithm.
     6.5  *)
     6.6  
     6.7 -signature CODE_FUNCGR =
     6.8 +signature CODE_WELLSORTED =
     6.9  sig
    6.10    type T
    6.11    val eqns: T -> string -> (thm * bool) list
    6.12 @@ -20,7 +20,7 @@
    6.13      -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    6.14  end
    6.15  
    6.16 -structure Code_Funcgr : CODE_FUNCGR =
    6.17 +structure Code_Wellsorted : CODE_WELLSORTED =
    6.18  struct
    6.19  
    6.20  (** the equation graph type **)