1.1 --- a/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Mon Mar 02 16:58:39 2009 +0100
     1.3 @@ -597,7 +597,7 @@
     1.4       of SOME tyco => stmt_datatypecons tyco
     1.5        | NONE => (case AxClass.class_of_param thy c
     1.6           of SOME class => stmt_classparam class
     1.7 -          | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
     1.8 +          | NONE => stmt_fun (Code_Wellsorted.typ funcgr c, Code_Wellsorted.eqns funcgr c))
     1.9    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    1.10  and translate_term thy algbr funcgr thm (Const (c, ty)) =
    1.11        translate_app thy algbr funcgr thm ((c, ty), [])
    1.12 @@ -622,7 +622,7 @@
    1.13  and translate_const thy algbr funcgr thm (c, ty) =
    1.14    let
    1.15      val tys = Sign.const_typargs thy (c, ty);
    1.16 -    val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
    1.17 +    val sorts = (map snd o fst o Code_Wellsorted.typ funcgr) c;
    1.18      val tys_args = (fst o Term.strip_type) ty;
    1.19    in
    1.20      ensure_const thy algbr funcgr c
    1.21 @@ -735,7 +735,7 @@
    1.22      fun generate_consts thy algebra funcgr =
    1.23        fold_map (ensure_const thy algebra funcgr);
    1.24    in
    1.25 -    invoke_generation thy (Code_Funcgr.make thy cs) generate_consts cs
    1.26 +    invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
    1.27      |-> project_consts
    1.28    end;
    1.29  
    1.30 @@ -778,8 +778,8 @@
    1.31        in evaluator'' naming program vs_ty_t deps end;
    1.32    in (t', evaluator') end
    1.33  
    1.34 -fun eval_conv thy = Code_Funcgr.eval_conv thy o eval thy;
    1.35 -fun eval_term thy = Code_Funcgr.eval_term thy o eval thy;
    1.36 +fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
    1.37 +fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
    1.38  
    1.39  end; (*struct*)
    1.40