# HG changeset patch # User wenzelm # Date 1425682334 -3600 # Node ID a372513af1e23911afcb5e980f3caedc07afea54 # Parent 5980e75a204e53ab5519733aff687b36daedc045 clarified context; diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Mar 06 23:44:57 2015 +0100 +++ b/src/Tools/Code/code_preproc.ML Fri Mar 06 23:52:14 2015 +0100 @@ -153,12 +153,11 @@ fun evaluation sandwich lift_postproc eval ctxt t = let - val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt); - val (postproc, ct') = sandwich ctxt (cert t); + val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t); in Thm.term_of ct' |> eval ctxt - |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o cert) + |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o Thm.cterm_of ctxt) end; end; @@ -168,7 +167,6 @@ fun normalized_tfrees_sandwich ctxt ct = let - val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt); val t = Thm.term_of ct; val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; @@ -179,15 +177,15 @@ in if eq_list (eq_fst (op =)) (vs_normalized, vs_original) then (I, ct) - else (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t)) + else + (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, + Thm.cterm_of ctxt (map_types normalize t)) end; fun no_variables_sandwich ctxt ct = let - val thy = Proof_Context.theory_of ctxt; - val cert = Thm.global_cterm_of thy; - val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t) - | t as Var _ => insert (op aconvc) (cert t) + val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (Thm.cterm_of ctxt t) + | t as Var _ => insert (op aconvc) (Thm.cterm_of ctxt t) | _ => I) (Thm.term_of ct) []; fun apply_beta var thm = Thm.combination thm (Thm.reflexive var) |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Mar 06 23:44:57 2015 +0100 +++ b/src/Tools/Code/code_runtime.ML Fri Mar 06 23:52:14 2015 +0100 @@ -172,12 +172,11 @@ fun check_holds ctxt evaluator vs_t ct = let - val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; val _ = if fastype_of t <> propT - then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) + then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t) else (); - val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); + val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT)); val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t []) of SOME Holds => true | _ => false; diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Fri Mar 06 23:44:57 2015 +0100 +++ b/src/Tools/Code/code_simp.ML Fri Mar 06 23:52:14 2015 +0100 @@ -83,7 +83,7 @@ THEN' conclude_tac ctxt NONE ctxt; fun dynamic_value ctxt = - snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.global_cterm_of (Proof_Context.theory_of ctxt); + snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of ctxt; val _ = Theory.setup (Method.setup @{binding code_simp} diff -r 5980e75a204e -r a372513af1e2 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Mar 06 23:44:57 2015 +0100 +++ b/src/Tools/Code/code_thingol.ML Fri Mar 06 23:52:14 2015 +0100 @@ -574,7 +574,7 @@ let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); val dom_length = length (fst (strip_type ty)) - val thm = Axclass.unoverload_conv thy (Thm.global_cterm_of thy raw_const); + val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in