src/Tools/nbe.ML
changeset 42361 23f352990944
parent 41472 f6ab14e61604
child 42405 13ecdb3057d8
     1.1 --- a/src/Tools/nbe.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4  fun compile_eqnss thy nbe_program raw_deps [] = []
     1.5    | compile_eqnss thy nbe_program raw_deps eqnss =
     1.6        let
     1.7 -        val ctxt = ProofContext.init_global thy;
     1.8 +        val ctxt = Proof_Context.init_global thy;
     1.9          val (deps, deps_vals) = split_list (map_filter
    1.10            (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
    1.11          val idx_of = raw_deps
    1.12 @@ -615,7 +615,7 @@
    1.13  
    1.14  (** setup **)
    1.15  
    1.16 -val setup = Value.add_evaluator ("nbe", dynamic_value o ProofContext.theory_of);
    1.17 +val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of);
    1.18  
    1.19  end;
    1.20   
    1.21 \ No newline at end of file