src/Tools/Code/code_runtime.ML
changeset 42361 23f352990944
parent 42359 6ca5407863ed
child 43560 d1650e3720fd
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -83,14 +83,14 @@
     1.4  
     1.5  fun reject_vars thy t =
     1.6    let
     1.7 -    val ctxt = ProofContext.init_global thy;
     1.8 +    val ctxt = Proof_Context.init_global thy;
     1.9    in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
    1.10  
    1.11  fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
    1.12  
    1.13  fun evaluation cookie thy evaluator vs_t args =
    1.14    let
    1.15 -    val ctxt = ProofContext.init_global thy;
    1.16 +    val ctxt = Proof_Context.init_global thy;
    1.17      val (program_code, value_name) = evaluator vs_t;
    1.18      val value_code = space_implode " "
    1.19        (value_name :: "()" :: map (enclose "(" ")") args);
    1.20 @@ -188,7 +188,7 @@
    1.21  
    1.22  fun evaluation_code thy module_name tycos consts =
    1.23    let
    1.24 -    val ctxt = ProofContext.init_global thy;
    1.25 +    val ctxt = Proof_Context.init_global thy;
    1.26      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    1.27      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    1.28      val (ml_code, target_names) =
    1.29 @@ -202,7 +202,7 @@
    1.30         | SOME const'' => (const, const'')) consts consts''
    1.31      val tycos_map = map2 (fn tyco =>
    1.32        fn NONE =>
    1.33 -          error ("Type " ^ quote (ProofContext.extern_type ctxt tyco) ^
    1.34 +          error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
    1.35              "\nhas a user-defined serialization")
    1.36          | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
    1.37    in (ml_code, (tycos_map, consts_map)) end;
    1.38 @@ -227,7 +227,7 @@
    1.39      val tycos' = fold (insert (op =)) new_tycos tycos;
    1.40      val consts' = fold (insert (op =)) new_consts consts;
    1.41      val acc_code = Lazy.lazy (fn () =>
    1.42 -      evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts'
    1.43 +      evaluation_code (Proof_Context.theory_of ctxt) "Code" tycos' consts'
    1.44        |> apsnd snd);
    1.45    in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end;
    1.46  
    1.47 @@ -245,7 +245,7 @@
    1.48  
    1.49  fun ml_code_antiq raw_const background =
    1.50    let
    1.51 -    val const = Code.check_const (ProofContext.theory_of background) raw_const;
    1.52 +    val const = Code.check_const (Proof_Context.theory_of background) raw_const;
    1.53      val is_first = is_first_occ background;
    1.54      val background' = register_const const background;
    1.55    in (print_code is_first const, background') end;