# HG changeset patch # User wenzelm # Date 1251486243 -7200 # Node ID 64f30bdd3ba1be08057692626b779336cfa663e5 # Parent bcd14373ec30edced2604ce3e8f9416d16eaed92 modernized messages -- eliminated ctyp/cterm operations; diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Fri Aug 28 21:04:03 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 () diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri Aug 28 21:04:03 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")) ^ diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Fri Aug 28 21:04:03 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) diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Statespace/state_space.ML Fri Aug 28 21:04:03 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)) diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Fri Aug 28 21:04:03 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 diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Fri Aug 28 21:04:03 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 diff -r bcd14373ec30 -r 64f30bdd3ba1 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Fri Aug 28 21:04:03 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 *) diff -r bcd14373ec30 -r 64f30bdd3ba1 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/Pure/old_goals.ML Fri Aug 28 21:04:03 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.*) diff -r bcd14373ec30 -r 64f30bdd3ba1 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Aug 28 18:23:24 2009 +0200 +++ b/src/Tools/induct.ML Fri Aug 28 21:04:03 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))) diff -r bcd14373ec30 -r 64f30bdd3ba1 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Fri Aug 28 18:23:24 2009 +0200 +++ b/src/ZF/Datatype_ZF.thy Fri Aug 28 21:04:03 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