--- a/NEWS Fri Aug 28 20:49:53 2009 +0200
+++ b/NEWS Fri Aug 28 21:44:48 2009 +0200
@@ -181,6 +181,10 @@
or even Display.pretty_thm_without_context as last resort.
INCOMPATIBILITY.
+* Discontinued Display.pretty_ctyp/cterm etc. INCOMPATIBILITY, use
+Syntax.pretty_typ/term directly, preferably with proper context
+instead of global theory.
+
*** System ***
--- a/src/HOL/Import/hol4rews.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Aug 28 21:44:48 2009 +0200
@@ -531,7 +531,7 @@
val _ = app (fn (hol,(internal,isa,opt_ty)) =>
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
case opt_ty of
- SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"")
+ SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
| NONE => ())) constmaps
val _ = if null constmaps
then ()
--- a/src/HOL/Import/proof_kernel.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Aug 28 21:44:48 2009 +0200
@@ -199,12 +199,12 @@
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
in
- quote(
+ quote (
PrintMode.setmp [] (
Library.setmp show_brackets false (
Library.setmp show_all_types true (
Library.setmp Syntax.ambiguity_is_error false (
- Library.setmp show_sorts true Display.string_of_cterm))))
+ Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
ct)
end
@@ -226,7 +226,8 @@
| G _ = raise SMART_STRING
fun F n =
let
- val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
+ val str =
+ Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
|> TypeInfer.constrain T |> Syntax.check_term ctxt
in
@@ -234,8 +235,9 @@
then quote str
else F (n+1)
end
- handle ERROR mesg => F (n+1)
- | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
+ handle ERROR mesg => F (n + 1)
+ | SMART_STRING =>
+ error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
in
PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
@@ -243,8 +245,7 @@
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
-fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
+fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
fun prin t = writeln (PrintMode.setmp []
(fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
@@ -1939,16 +1940,17 @@
then
let
val p1 = quotename constname
- val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
+ val p2 = Syntax.string_of_typ_global thy'' ctype
val p3 = string_of_mixfix csyn
val p4 = smart_string_of_cterm crhs
in
- add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
+ add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy''
end
else
- (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
- "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
- thy'')
+ add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
+ Syntax.string_of_typ_global thy'' ctype ^
+ "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^
+ quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
SOME (_,res) => HOLThm(rens_of linfo,res)
| NONE => raise ERR "new_definition" "Bad conclusion"
@@ -2008,8 +2010,9 @@
in
((cname,cT,mk_syn thy cname)::cs,p)
end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
- val str = Library.foldl (fn (acc,(c,T,csyn)) =>
- acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
+ val str = Library.foldl (fn (acc, (c, T, csyn)) =>
+ acc ^ "\n " ^ quotename c ^ " :: \"" ^
+ Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
val thy' = add_dump str thy
val _ = ImportRecorder.add_consts consts
in
@@ -2137,7 +2140,7 @@
fun add_dump_constdefs thy defname constname rhs ty =
let
val n = quotename constname
- val t = Display.string_of_ctyp (ctyp_of thy ty)
+ val t = Syntax.string_of_typ_global thy ty
val syn = string_of_mixfix (mk_syn thy constname)
(*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
val eq = quote (constname ^ " == "^rhs)
@@ -2224,7 +2227,7 @@
(" apply (rule light_ex_imp_nonempty[where t="^
(proc_prop (cterm_of thy4 t))^"])\n"^
(" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
- val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
+ val str_aty = Syntax.string_of_typ_global thy aty
val thy = add_dump_syntax thy rep_name
val thy = add_dump_syntax thy abs_name
val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
--- a/src/HOL/Import/shuffler.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Fri Aug 28 21:44:48 2009 +0200
@@ -57,7 +57,6 @@
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
-val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun mk_meta_eq th =
(case concl_of th of
@@ -304,13 +303,14 @@
val lhs = #1 (Logic.dest_equals (prop_of (final init)))
in
if not (lhs aconv origt)
- then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (Display.string_of_cterm (cterm_of thy origt));
- writeln (Display.string_of_cterm (cterm_of thy lhs));
- writeln (Display.string_of_cterm (cterm_of thy typet));
- writeln (Display.string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
- writeln "done")
+ then
+ writeln (cat_lines
+ (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+ Syntax.string_of_term_global thy origt,
+ Syntax.string_of_term_global thy lhs,
+ Syntax.string_of_term_global thy typet,
+ Syntax.string_of_term_global thy t] @
+ map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
else ()
end
in
@@ -366,13 +366,14 @@
val lhs = #1 (Logic.dest_equals (prop_of (final init)))
in
if not (lhs aconv origt)
- then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (Display.string_of_cterm (cterm_of thy origt));
- writeln (Display.string_of_cterm (cterm_of thy lhs));
- writeln (Display.string_of_cterm (cterm_of thy typet));
- writeln (Display.string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
- writeln "done")
+ then
+ writeln (cat_lines
+ (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+ Syntax.string_of_term_global thy origt,
+ Syntax.string_of_term_global thy lhs,
+ Syntax.string_of_term_global thy typet,
+ Syntax.string_of_term_global thy t] @
+ map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
else ()
end
in
@@ -407,9 +408,8 @@
end
| _ => NONE)
else NONE
- | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
- end
- handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
+ | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
+ end;
fun mk_tfree s = TFree("'"^s,[])
fun mk_free s t = Free (s,t)
--- a/src/HOL/Statespace/state_space.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML Fri Aug 28 21:44:48 2009 +0200
@@ -567,8 +567,8 @@
(case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
[] => []
| [_] => []
- | rs => ["Different types for component " ^ n ^": " ^ commas
- (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
+ | rs => ["Different types for component " ^ n ^": " ^
+ commas (map (Syntax.string_of_typ ctxt o snd) rs)])
val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
--- a/src/HOL/Tools/TFL/tfl.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Fri Aug 28 21:44:48 2009 +0200
@@ -8,7 +8,7 @@
sig
val trace: bool ref
val trace_thms: string -> thm list -> unit
- val trace_cterms: string -> cterm list -> unit
+ val trace_cterm: 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
@@ -296,7 +296,7 @@
raise TFL_ERR "no_repeat_vars"
(quote (#1 (dest_Free v)) ^
" occurs repeatedly in the pattern " ^
- quote (Display.string_of_cterm (Thry.typecheck thy pat)))
+ quote (Syntax.string_of_term_global thy pat))
else check rst
in check (FV_multiset pat)
end;
@@ -912,9 +912,10 @@
if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
else ();
-fun trace_cterms s L =
- if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
- else ();;
+fun trace_cterm s ct =
+ if !trace then
+ writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
+ else ();
fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
@@ -942,7 +943,7 @@
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
- val _ = trace_cterms "TC before simplification: " [tc1]
+ val _ = trace_cterm "TC before simplification: " tc1
val tc_eq = simplifier tc1
val _ = trace_thms "result: " [tc_eq]
in
--- a/src/HOL/Tools/metis_tools.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Fri Aug 28 21:44:48 2009 +0200
@@ -299,7 +299,7 @@
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
that new TVars are distinct and that types can be inferred from terms.*)
- fun inst_inf ctxt thpairs fsubst th =
+ fun inst_inf ctxt thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -324,11 +324,12 @@
val tms = infer_types ctxt rawtms;
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
- val _ = Output.debug (fn() => "subst_translations:")
- val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
- Display.string_of_cterm y))
- substs'
- in cterm_instantiate substs' i_th
+ val _ = Output.debug (fn () =>
+ cat_lines ("subst_translations:" ::
+ (substs' |> map (fn (x, y) =>
+ Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
+ Syntax.string_of_term ctxt (term_of y)))));
+ in cterm_instantiate substs' i_th
handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
end;
@@ -610,14 +611,14 @@
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
- (_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+ (_,ith)::_ =>
+ (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (Output.debug (fn () => "Metis: no result");
+ | _ => (Output.debug (fn () => "Metis: no result");
[])
end
- | Metis.Resolution.Satisfiable _ =>
- (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
+ | Metis.Resolution.Satisfiable _ =>
+ (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
[])
end;
@@ -625,9 +626,9 @@
let val _ = Output.debug (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
+ if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
- else
+ else
(Meson.MESON ResAxioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
THEN ResAxioms.expand_defs_tac st0) st0
--- a/src/HOL/Tools/sat_funcs.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri Aug 28 21:44:48 2009 +0200
@@ -51,7 +51,7 @@
val trace_sat: bool ref (* input: print trace messages *)
val solver: string ref (* input: name of SAT solver to be used *)
val counter: int ref (* output: number of resolution steps during last proof replay *)
- val rawsat_thm: cterm list -> thm
+ val rawsat_thm: Proof.context -> cterm list -> thm
val rawsat_tac: Proof.context -> int -> tactic
val sat_tac: Proof.context -> int -> tactic
val satx_tac: Proof.context -> int -> tactic
@@ -295,9 +295,7 @@
(* hyps). *)
(* ------------------------------------------------------------------------- *)
-(* Thm.cterm list -> Thm.thm *)
-
-fun rawsat_thm clauses =
+fun rawsat_thm ctxt clauses =
let
(* remove premises that equal "True" *)
val clauses' = filter (fn clause =>
@@ -310,7 +308,7 @@
((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
handle TERM ("dest_Trueprop", _) => false)
orelse (
- warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
+ warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
false)) clauses'
(* remove trivial clauses -- this is necessary because zChaff removes *)
(* trivial clauses during preprocessing, and otherwise our clause *)
@@ -323,7 +321,8 @@
(* sorted in ascending order *)
val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
val _ = if !trace_sat then
- tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
+ tracing ("Sorted non-trivial clauses:\n" ^
+ cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
else ()
(* translate clauses from HOL terms to PropLogic.prop_formula *)
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
@@ -411,7 +410,8 @@
(* ------------------------------------------------------------------------- *)
fun rawsat_tac ctxt i =
- Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+ Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+ rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/Pure/display.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/Pure/display.ML Fri Aug 28 21:44:48 2009 +0200
@@ -27,10 +27,6 @@
val string_of_thm_without_context: thm -> string
val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
- val pretty_ctyp: ctyp -> Pretty.T
- val string_of_ctyp: ctyp -> string
- val pretty_cterm: cterm -> Pretty.T
- val string_of_cterm: cterm -> string
val print_syntax: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T list
end;
@@ -119,15 +115,6 @@
fun pretty_thms ctxt = pretty_thms_aux ctxt true;
-(* other printing commands *)
-
-fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-
-fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
-fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
-
-
(** print theory **)
--- a/src/Pure/old_goals.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/Pure/old_goals.ML Fri Aug 28 21:44:48 2009 +0200
@@ -362,10 +362,7 @@
(case Seq.pull (tac st0) of
SOME(st,_) => st
| _ => error ("prove_goal: tactic failed"))
- in mkresult (check, cond_timeit (!Output.timing) "" statef) end
- handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
- writeln ("The exception above was raised for\n" ^
- Display.string_of_cterm chorn); raise e);
+ in mkresult (check, cond_timeit (!Output.timing) "" statef) end;
(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)
--- a/src/Tools/induct.ML Fri Aug 28 20:49:53 2009 +0200
+++ b/src/Tools/induct.ML Fri Aug 28 21:44:48 2009 +0200
@@ -288,21 +288,21 @@
(* prep_inst *)
-fun prep_inst thy align tune (tm, ts) =
+fun prep_inst ctxt align tune (tm, ts) =
let
- val cert = Thm.cterm_of thy;
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
fun prep_var (x, SOME t) =
let
val cx = cert x;
val xT = #T (Thm.rep_cterm cx);
val ct = cert (tune t);
- val tT = Thm.ctyp_of_term ct;
+ val tT = #T (Thm.rep_cterm ct);
in
- if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
+ if Type.could_unify (tT, xT) then SOME (cx, ct)
else error (Pretty.string_of (Pretty.block
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
- Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
- Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
+ Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
+ Syntax.pretty_typ ctxt tT]))
end
| prep_var (_, NONE) = NONE;
val xs = vars_of tm;
@@ -342,12 +342,11 @@
fun cases_tac ctxt insts opt_rule facts =
let
val thy = ProofContext.theory_of ctxt;
- val cert = Thm.cterm_of thy;
fun inst_rule r =
if null insts then `RuleCases.get r
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
- |> maps (prep_inst thy align_left I)
+ |> maps (prep_inst ctxt align_left I)
|> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
val ruleq =
@@ -411,8 +410,8 @@
(* prepare rule *)
-fun rule_instance thy inst rule =
- Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
+fun rule_instance ctxt inst rule =
+ Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
fun internalize k th =
th |> Thm.permute_prems 0 k
@@ -589,7 +588,7 @@
(if null insts then `RuleCases.get r
else (align_left "Rule has fewer conclusions than arguments given"
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
- |> maps (prep_inst thy align_right (atomize_term thy))
+ |> maps (prep_inst ctxt align_right (atomize_term thy))
|> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
@@ -619,7 +618,7 @@
THEN' inner_atomize_tac) j))
THEN' atomize_tac) i st |> Seq.maps (fn st' =>
guess_instance ctxt (internalize more_consumes rule) i st'
- |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
+ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (rule_cases rule' cases)
(Tactic.rtac rule' i THEN
@@ -657,7 +656,7 @@
fun inst_rule r =
if null inst then `RuleCases.get r
- else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
+ else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
|> pair (RuleCases.get r);
fun ruleq goal =
@@ -673,7 +672,7 @@
|> Seq.maps (RuleCases.consume [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
guess_instance ctxt rule i st
- |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
+ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
(Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
--- a/src/ZF/Datatype_ZF.thy Fri Aug 28 20:49:53 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Fri Aug 28 21:44:48 2009 +0200
@@ -14,9 +14,9 @@
(*Typechecking rules for most datatypes involving univ*)
structure Data_Arg =
struct
- val intrs =
+ val intrs =
[@{thm SigmaI}, @{thm InlI}, @{thm InrI},
- @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
+ @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
@{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
@@ -25,7 +25,7 @@
end;
-structure Data_Package =
+structure Data_Package =
Add_datatype_def_Fun
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
and Su=Standard_Sum
@@ -37,16 +37,16 @@
(*Typechecking rules for most codatatypes involving quniv*)
structure CoData_Arg =
struct
- val intrs =
+ val intrs =
[@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
- @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
+ @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
@{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD}, (*for mutual recursion*)
@{thm QSigmaE}, @{thm qsumE}]; (*allows * and + in spec*)
end;
-structure CoData_Package =
+structure CoData_Package =
Add_datatype_def_Fun
(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
and Su=Quine_Sum
@@ -69,9 +69,9 @@
val datatype_ss = @{simpset};
fun proc sg ss old =
- let val _ = if !trace then writeln ("data_free: OLD = " ^
- Display.string_of_cterm (cterm_of sg old))
- else ()
+ let val _ =
+ if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
+ else ()
val (lhs,rhs) = FOLogic.dest_eq old
val (lhead, largs) = strip_comb lhs
and (rhead, rargs) = strip_comb rhs
@@ -81,15 +81,15 @@
handle Option => raise Match;
val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
handle Option => raise Match;
- val new =
- if #big_rec_name lcon_info = #big_rec_name rcon_info
+ val new =
+ if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
else Const("False",FOLogic.oT)
else raise Match
- val _ = if !trace then
- writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
- else ();
+ val _ =
+ if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
+ else ();
val goal = Logic.mk_equals (old, new)
val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
(fn _ => rtac iff_reflection 1 THEN