--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 18:42:46 2014 +0100
@@ -12,7 +12,7 @@
val is_zapped_var_name : string -> bool
val is_quasi_lambda_free : term -> bool
val introduce_combinators_in_cterm : cterm -> thm
- val introduce_combinators_in_theorem : thm -> thm
+ val introduce_combinators_in_theorem : Proof.context -> thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val ss_only : thm list -> Proof.context -> Proof.context
val cnf_axiom :
@@ -163,7 +163,7 @@
(introduce_combinators_in_cterm ct2)
end
-fun introduce_combinators_in_theorem th =
+fun introduce_combinators_in_theorem ctxt th =
if is_quasi_lambda_free (prop_of th) then
th
else
@@ -173,7 +173,7 @@
in Thm.equal_elim eqth th end
handle THM (msg, _, _) =>
(warning ("Error in the combinator translation of " ^
- Display.string_of_thm_without_context th ^
+ Display.string_of_thm ctxt th ^
"\nException message: " ^ msg ^ ".");
(* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
@@ -387,7 +387,7 @@
(opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
##> (term_of #> HOLogic.dest_Trueprop
#> singleton (Variable.export_terms ctxt ctxt0))),
- cnf_ths |> map (combinators ? introduce_combinators_in_theorem
+ cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
|> Variable.export ctxt ctxt0
|> finish_cnf
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 18:42:46 2014 +0100
@@ -238,7 +238,7 @@
fun neg_clausify ctxt combinators =
single
#> Meson.make_clauses_unsorted ctxt
- #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
+ #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
--- a/src/HOL/Tools/TFL/casesplit.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML Sat Feb 01 18:42:46 2014 +0100
@@ -128,8 +128,8 @@
(case find_thms_split splitths 1 th of
NONE =>
(writeln (cat_lines
- (["th:", Display.string_of_thm_without_context th, "split ths:"] @
- map Display.string_of_thm_without_context splitths @ ["\n--"]));
+ (["th:", Display.string_of_thm ctxt th, "split ths:"] @
+ map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
--- a/src/HOL/Tools/TFL/post.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sat Feb 01 18:42:46 2014 +0100
@@ -101,14 +101,12 @@
if (solved th) then (th::So, Si, St)
else (So, th::Si, St)) nested_tcs ([],[],[])
val simplified' = map (join_assums ctxt) simplified
- val dummy = (Prim.trace_thms "solved =" solved;
- Prim.trace_thms "simplified' =" simplified')
+ val dummy = (Prim.trace_thms ctxt "solved =" solved;
+ Prim.trace_thms ctxt "simplified' =" simplified')
val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
- val dummy = Prim.trace_thms "Simplifying the induction rule..."
- [induction]
+ val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
val induction' = rewr induction
- val dummy = Prim.trace_thms "Simplifying the recursion rules..."
- [rules]
+ val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
val rules' = rewr rules
val _ = writeln "... Postprocessing finished";
in
@@ -142,7 +140,7 @@
Prim.post_definition congs thy ctxt (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
- val dummy = Prim.trace_thms "congs =" congs
+ val dummy = Prim.trace_thms ctxt "congs =" congs
(*the next step has caused simplifier looping in some cases*)
val {induction, rules, tcs} =
proof_stage strict ctxt wfs thy
--- a/src/HOL/Tools/TFL/rules.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Sat Feb 01 18:42:46 2014 +0100
@@ -535,11 +535,11 @@
fun say s = if !tracing then writeln s else ();
-fun print_thms s L =
- say (cat_lines (s :: map Display.string_of_thm_without_context L));
+fun print_thms ctxt s L =
+ say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
-fun print_cterm s ct =
- say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
+fun print_cterm ctxt s ct =
+ say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]);
(*---------------------------------------------------------------------------
@@ -656,20 +656,20 @@
let fun cong_prover ctxt thm =
let val dummy = say "cong_prover:"
val cntxt = Simplifier.prems_of ctxt
- val dummy = print_thms "cntxt:" cntxt
+ val dummy = print_thms ctxt "cntxt:" cntxt
val dummy = say "cong rule:"
- val dummy = say (Display.string_of_thm_without_context thm)
+ val dummy = say (Display.string_of_thm ctxt thm)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp,thy) =
let val tych = cterm_of thy
- val dummy = print_cterm "To eliminate:" (tych imp)
+ val dummy = print_cterm ctxt "To eliminate:" (tych imp)
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
handle Utils.ERR _ => Thm.reflexive lhs
- val dummy = print_thms "proven:" [lhs_eq_lhs1]
+ val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
in
@@ -738,7 +738,7 @@
fun restrict_prover ctxt thm =
let val dummy = say "restrict_prover:"
val cntxt = rev (Simplifier.prems_of ctxt)
- val dummy = print_thms "cntxt:" cntxt
+ val dummy = print_thms ctxt "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
@@ -760,8 +760,8 @@
val antl = case rcontext of [] => []
| _ => [USyntax.list_mk_conj(map cncl rcontext)]
val TC = genl(USyntax.list_mk_imp(antl, A))
- val dummy = print_cterm "func:" (cterm_of thy func)
- val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
+ val dummy = print_cterm ctxt "func:" (cterm_of thy func)
+ val dummy = print_cterm ctxt "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
val dummy = tc_list := (TC :: !tc_list)
val nestedp = is_some (USyntax.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
--- a/src/HOL/Tools/TFL/tfl.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Sat Feb 01 18:42:46 2014 +0100
@@ -7,8 +7,8 @@
signature PRIM =
sig
val trace: bool Unsynchronized.ref
- val trace_thms: string -> thm list -> unit
- val trace_cterm: string -> cterm -> unit
+ val trace_thms: Proof.context -> string -> thm list -> unit
+ val trace_cterm: Proof.context -> string -> cterm -> unit
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
val wfrec_definition0: theory -> string -> term -> term -> theory * thm
@@ -901,18 +901,19 @@
(Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
-fun trace_thms s L =
- if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
+fun trace_thms ctxt s L =
+ if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
else ();
-fun trace_cterm s ct =
+fun trace_cterm ctxt s ct =
if !trace then
- writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
+ writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
else ();
fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
-let val tych = Thry.typecheck theory
+let val ctxt = Proof_Context.init_global theory;
+ val tych = Thry.typecheck theory;
val prove = Rules.prove strict;
(*---------------------------------------------------------------------
@@ -936,9 +937,9 @@
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
- val _ = trace_cterm "TC before simplification: " tc1
+ val _ = trace_cterm ctxt "TC before simplification: " tc1
val tc_eq = simplifier tc1
- val _ = trace_thms "result: " [tc_eq]
+ val _ = trace_thms ctxt "result: " [tc_eq]
in
elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
handle Utils.ERR _ =>
--- a/src/HOL/Tools/numeral.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/numeral.ML Sat Feb 01 18:42:46 2014 +0100
@@ -71,10 +71,10 @@
let
fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
| dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
- | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
+ | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
- | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
+ | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
in if negative then ~ (dest_num t) else dest_num t end;
fun pretty literals _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o dest_numeral thm) t;
--- a/src/HOL/Tools/sat_funcs.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Sat Feb 01 18:42:46 2014 +0100
@@ -117,9 +117,9 @@
(* cterms. *)
(* ------------------------------------------------------------------------- *)
-fun resolve_raw_clauses [] =
+fun resolve_raw_clauses _ [] =
raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
- | resolve_raw_clauses (c::cs) =
+ | resolve_raw_clauses ctxt (c::cs) =
let
(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
fun merge xs [] = xs
@@ -154,10 +154,10 @@
let
val _ =
if ! trace_sat then (* FIXME !? *)
- tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
+ tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
" (hyps: " ^ ML_Syntax.print_list
(Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
- ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
+ ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
" (hyps: " ^ ML_Syntax.print_list
(Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
else ()
@@ -178,7 +178,7 @@
val _ =
if !trace_sat then
- tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
+ tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
else ()
(* Gamma1, Gamma2 |- False *)
@@ -189,7 +189,7 @@
val _ =
if !trace_sat then
- tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
+ tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
" (hyps: " ^ ML_Syntax.print_list
(Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
else ()
@@ -211,7 +211,7 @@
(* occur (as part of a literal) in 'clauses' to positive integers. *)
(* ------------------------------------------------------------------------- *)
-fun replay_proof atom_table clauses (clause_table, empty_id) =
+fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
let
fun index_of_literal chyp =
(case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
@@ -242,7 +242,7 @@
val _ =
if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
val ids = the (Inttab.lookup clause_table id)
- val clause = resolve_raw_clauses (map prove_clause ids)
+ val clause = resolve_raw_clauses ctxt (map prove_clause ids)
val _ = Array.update (clauses, id, RAW_CLAUSE clause)
val _ =
if !trace_sat then
@@ -372,7 +372,7 @@
cnf_clauses 0
(* replay the proof to derive the empty clause *)
(* [c_1 && ... && c_n] |- False *)
- val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
+ val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
in
(* [c_1, ..., c_n] |- False *)
Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
--- a/src/HOL/Tools/string_code.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/HOL/Tools/string_code.ML Sat Feb 01 18:42:46 2014 +0100
@@ -62,28 +62,28 @@
[(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end;
-fun add_literal_char target =
+fun add_literal_char target thy =
let
fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
case decode_char (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
- | NONE => Code_Printer.eqn_error thm "Illegal character expression";
+ | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
- [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) thy
end;
-fun add_literal_string target =
+fun add_literal_string target thy =
let
fun pretty literals _ thm _ _ [(t, _)] =
case List_Code.implode_list t
of SOME ts => (case implode_string literals ts
of SOME p => p
- | NONE => Code_Printer.eqn_error thm "Illegal string literal expression")
- | NONE => Code_Printer.eqn_error thm "Illegal string literal expression";
+ | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
+ | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
- [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) thy
end;
end;
--- a/src/Tools/Code/code_printer.ML Sat Feb 01 18:41:48 2014 +0100
+++ b/src/Tools/Code/code_printer.ML Sat Feb 01 18:42:46 2014 +0100
@@ -11,7 +11,7 @@
type const = Code_Thingol.const
type dict = Code_Thingol.dict
- val eqn_error: thm option -> string -> 'a
+ val eqn_error: theory -> thm option -> string -> 'a
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
@@ -100,9 +100,9 @@
(** generic nonsense *)
-fun eqn_error (SOME thm) s =
- error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
- | eqn_error NONE s = error s;
+fun eqn_error thy (SOME thm) s =
+ error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
+ | eqn_error _ NONE s = error s;
val code_presentationN = "code_presentation";
val stmt_nameN = "stmt_name";