clarified context;
authorwenzelm
Fri Mar 06 23:52:14 2015 +0100 (2015-03-06)
changeset 59633a372513af1e2
parent 59632 5980e75a204e
child 59634 4b94cc030ba0
clarified context;
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Fri Mar 06 23:44:57 2015 +0100
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Mar 06 23:52:14 2015 +0100
     1.3 @@ -153,12 +153,11 @@
     1.4  
     1.5  fun evaluation sandwich lift_postproc eval ctxt t =
     1.6    let
     1.7 -    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     1.8 -    val (postproc, ct') = sandwich ctxt (cert t);
     1.9 +    val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
    1.10    in
    1.11      Thm.term_of ct'
    1.12      |> eval ctxt
    1.13 -    |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o cert)
    1.14 +    |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o Thm.cterm_of ctxt)
    1.15    end;
    1.16  
    1.17  end;
    1.18 @@ -168,7 +167,6 @@
    1.19  
    1.20  fun normalized_tfrees_sandwich ctxt ct =
    1.21    let
    1.22 -    val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
    1.23      val t = Thm.term_of ct;
    1.24      val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    1.25        o dest_TFree))) t [];
    1.26 @@ -179,15 +177,15 @@
    1.27    in
    1.28      if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
    1.29      then (I, ct)
    1.30 -    else (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
    1.31 +    else
    1.32 +     (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global,
    1.33 +      Thm.cterm_of ctxt (map_types normalize t))
    1.34    end;
    1.35  
    1.36  fun no_variables_sandwich ctxt ct =
    1.37    let
    1.38 -    val thy = Proof_Context.theory_of ctxt;
    1.39 -    val cert = Thm.global_cterm_of thy;
    1.40 -    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
    1.41 -      | t as Var _ => insert (op aconvc) (cert t)
    1.42 +    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (Thm.cterm_of ctxt t)
    1.43 +      | t as Var _ => insert (op aconvc) (Thm.cterm_of ctxt t)
    1.44        | _ => I) (Thm.term_of ct) [];
    1.45      fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
    1.46        |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
     2.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:44:57 2015 +0100
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:52:14 2015 +0100
     2.3 @@ -172,12 +172,11 @@
     2.4  
     2.5  fun check_holds ctxt evaluator vs_t ct =
     2.6    let
     2.7 -    val thy = Proof_Context.theory_of ctxt;
     2.8      val t = Thm.term_of ct;
     2.9      val _ = if fastype_of t <> propT
    2.10 -      then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    2.11 +      then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    2.12        else ();
    2.13 -    val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    2.14 +    val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    2.15      val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
    2.16       of SOME Holds => true
    2.17        | _ => false;
     3.1 --- a/src/Tools/Code/code_simp.ML	Fri Mar 06 23:44:57 2015 +0100
     3.2 +++ b/src/Tools/Code/code_simp.ML	Fri Mar 06 23:52:14 2015 +0100
     3.3 @@ -83,7 +83,7 @@
     3.4    THEN' conclude_tac ctxt NONE ctxt;
     3.5  
     3.6  fun dynamic_value ctxt =
     3.7 -  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.global_cterm_of (Proof_Context.theory_of ctxt);
     3.8 +  snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of ctxt;
     3.9  
    3.10  val _ = Theory.setup 
    3.11    (Method.setup @{binding code_simp}
     4.1 --- a/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:44:57 2015 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:52:14 2015 +0100
     4.3 @@ -574,7 +574,7 @@
     4.4        let
     4.5          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
     4.6          val dom_length = length (fst (strip_type ty))
     4.7 -        val thm = Axclass.unoverload_conv thy (Thm.global_cterm_of thy raw_const);
     4.8 +        val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const);
     4.9          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
    4.10            o Logic.dest_equals o Thm.prop_of) thm;
    4.11        in