src/Provers/classical.ML
changeset 32091 30e2ffbba718
parent 31945 d5f186aa0bed
child 32148 253f6808dabe
     1.1 --- a/src/Provers/classical.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -256,7 +256,7 @@
     1.4       xtra_netpair  = empty_netpair};
     1.5  
     1.6  fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
     1.7 -  let val pretty_thms = map Display.pretty_thm in
     1.8 +  let val pretty_thms = map Display.pretty_thm_without_context in
     1.9      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
    1.10        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
    1.11        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
    1.12 @@ -313,14 +313,18 @@
    1.13  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    1.14    is still allowed.*)
    1.15  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
    1.16 -       if mem_thm safeIs th then
    1.17 -         warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
    1.18 +  if mem_thm safeIs th then
    1.19 +    warning ("Rule already declared as safe introduction (intro!)\n" ^
    1.20 +      Display.string_of_thm_without_context th)
    1.21    else if mem_thm safeEs th then
    1.22 -         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
    1.23 +    warning ("Rule already declared as safe elimination (elim!)\n" ^
    1.24 +      Display.string_of_thm_without_context th)
    1.25    else if mem_thm hazIs th then
    1.26 -         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
    1.27 +    warning ("Rule already declared as introduction (intro)\n" ^
    1.28 +      Display.string_of_thm_without_context th)
    1.29    else if mem_thm hazEs th then
    1.30 -         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
    1.31 +    warning ("Rule already declared as elimination (elim)\n" ^
    1.32 +      Display.string_of_thm_without_context th)
    1.33    else ();
    1.34  
    1.35  
    1.36 @@ -330,8 +334,8 @@
    1.37    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.38               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.39    if mem_thm safeIs th then
    1.40 -         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
    1.41 -          cs)
    1.42 +    (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
    1.43 +      Display.string_of_thm_without_context th); cs)
    1.44    else
    1.45    let val th' = flat_rule th
    1.46        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.47 @@ -356,10 +360,10 @@
    1.48    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.49               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.50    if mem_thm safeEs th then
    1.51 -         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
    1.52 -          cs)
    1.53 +    (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
    1.54 +        Display.string_of_thm_without_context th); cs)
    1.55    else if has_fewer_prems 1 th then
    1.56 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
    1.57 +    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
    1.58    else
    1.59    let
    1.60        val th' = classical_rule (flat_rule th)
    1.61 @@ -386,7 +390,7 @@
    1.62  
    1.63  fun make_elim th =
    1.64      if has_fewer_prems 1 th then
    1.65 -    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
    1.66 +    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
    1.67      else Tactic.make_elim th;
    1.68  
    1.69  fun cs addSDs ths = cs addSEs (map make_elim ths);
    1.70 @@ -398,8 +402,8 @@
    1.71    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.72               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.73    if mem_thm hazIs th then
    1.74 -         (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
    1.75 -          cs)
    1.76 +    (warning ("Ignoring duplicate introduction (intro)\n" ^
    1.77 +        Display.string_of_thm_without_context th); cs)
    1.78    else
    1.79    let val th' = flat_rule th
    1.80        val nI = length hazIs + 1
    1.81 @@ -418,16 +422,16 @@
    1.82          xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
    1.83    end
    1.84    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
    1.85 -         error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
    1.86 +    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
    1.87  
    1.88  fun addE w th
    1.89    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.90              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.91    if mem_thm hazEs th then
    1.92 -         (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
    1.93 -          cs)
    1.94 +    (warning ("Ignoring duplicate elimination (elim)\n" ^
    1.95 +        Display.string_of_thm_without_context th); cs)
    1.96    else if has_fewer_prems 1 th then
    1.97 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
    1.98 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
    1.99    else
   1.100    let
   1.101        val th' = classical_rule (flat_rule th)
   1.102 @@ -519,7 +523,7 @@
   1.103      end
   1.104   else cs
   1.105   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   1.106 -        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
   1.107 +   error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.108  
   1.109  
   1.110  fun delE th
   1.111 @@ -548,7 +552,7 @@
   1.112        mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.113        mem_thm safeEs th' orelse mem_thm hazEs th'
   1.114      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   1.115 -    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
   1.116 +    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
   1.117    end;
   1.118  
   1.119  fun cs delrules ths = fold delrule ths cs;