1.1 --- a/src/Pure/Isar/code.ML	Mon Jan 04 16:00:23 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Jan 04 16:00:24 2010 +0100
     1.3 @@ -76,8 +76,8 @@
     1.4  signature CODE_DATA =
     1.5  sig
     1.6    type T
     1.7 -  val change: theory -> (theory -> T -> T) -> T
     1.8 -  val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
     1.9 +  val change: theory -> (T -> T) -> T
    1.10 +  val change_yield: theory -> (T -> 'a * T) -> 'a * T
    1.11  end;
    1.12  
    1.13  signature PRIVATE_CODE =
    1.14 @@ -85,9 +85,9 @@
    1.15    include CODE
    1.16    val declare_data: Object.T -> serial
    1.17    val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.18 -    -> theory -> (theory -> 'a -> 'a) -> 'a
    1.19 +    -> theory -> ('a -> 'a) -> 'a
    1.20    val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
    1.21 -    -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
    1.22 +    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
    1.23  end;
    1.24  
    1.25  structure Code : PRIVATE_CODE =
    1.26 @@ -287,18 +287,20 @@
    1.27  fun change_yield_data (kind, mk, dest) theory f =
    1.28    let
    1.29      val dataref = (snd o Code_Data.get) theory;
    1.30 -    val (datatab, thy, thy_ref) = case Synchronized.value dataref
    1.31 -     of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
    1.32 -      | NONE => (Datatab.empty, theory, Theory.check_thy theory)
    1.33 +    val (datatab, thy_ref) = case Synchronized.value dataref
    1.34 +     of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref)
    1.35 +          then (datatab, thy_ref)
    1.36 +          else (Datatab.empty, Theory.check_thy theory)
    1.37 +      | NONE => (Datatab.empty, Theory.check_thy theory)
    1.38      val data = case Datatab.lookup datatab kind
    1.39       of SOME data => data
    1.40        | NONE => invoke_init kind;
    1.41 -    val result as (x, data') = f thy (dest data);
    1.42 +    val result as (x, data') = f (dest data);
    1.43      val _ = Synchronized.change dataref
    1.44        ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
    1.45    in result end;
    1.46  
    1.47 -fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
    1.48 +fun change_data ops theory f = change_yield_data ops theory (f #> pair ()) |> snd;
    1.49  
    1.50  end; (*local*)
    1.51  

     2.1 --- a/src/Tools/Code/code_preproc.ML	Mon Jan 04 16:00:23 2010 +0100
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Jan 04 16:00:24 2010 +0100
     2.3 @@ -282,7 +282,7 @@
     2.4     of SOME classess => (classess, ([], []))
     2.5      | NONE => let
     2.6          val all_classes = complete_proper_sort thy [class];
     2.7 -        val superclasses = remove (op =) class all_classes
     2.8 +        val superclasses = remove (op =) class all_classes;
     2.9          val classess = map (complete_proper_sort thy)
    2.10            (Sign.arity_sorts thy tyco [class]);
    2.11          val inst_params = inst_params thy tyco all_classes;
    2.12 @@ -454,8 +454,8 @@
    2.13  
    2.14  (** retrieval and evaluation interfaces **)
    2.15  
    2.16 -fun obtain theory cs ts = apsnd snd
    2.17 -  (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
    2.18 +fun obtain thy cs ts = apsnd snd
    2.19 +  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
    2.20  
    2.21  fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    2.22    let

     3.1 --- a/src/Tools/Code/code_thingol.ML	Mon Jan 04 16:00:23 2010 +0100
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jan 04 16:00:24 2010 +0100
     3.3 @@ -848,8 +848,8 @@
     3.4    val empty = (empty_naming, Graph.empty);
     3.5  );
     3.6  
     3.7 -fun invoke_generation theory (algebra, eqngr) f name =
     3.8 -  Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
     3.9 +fun invoke_generation thy (algebra, eqngr) f name =
    3.10 +  Program.change_yield thy (fn naming_program => (NONE, naming_program)
    3.11      |> f thy algebra eqngr name
    3.12      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
    3.13  

     4.1 --- a/src/Tools/nbe.ML	Mon Jan 04 16:00:23 2010 +0100
     4.2 +++ b/src/Tools/nbe.ML	Mon Jan 04 16:00:24 2010 +0100
     4.3 @@ -513,14 +513,15 @@
     4.4  
     4.5  (* compilation, evaluation and reification *)
     4.6  
     4.7 -fun compile_eval theory naming program vs_t deps =
     4.8 +fun compile_eval thy naming program vs_t deps =
     4.9    let
    4.10 +    val ctxt = ProofContext.init thy;
    4.11      val (_, (gr, (_, idx_tab))) =
    4.12 -      Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
    4.13 +      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
    4.14    in
    4.15      vs_t
    4.16 -    |> eval_term (ProofContext.init theory) gr deps
    4.17 -    |> term_of_univ theory program idx_tab
    4.18 +    |> eval_term ctxt gr deps
    4.19 +    |> term_of_univ thy program idx_tab
    4.20    end;
    4.21  
    4.22  (* evaluation with type reconstruction *)