modernized messages -- eliminated ctyp/cterm operations;
authorwenzelm
Fri Aug 28 21:04:03 2009 +0200 (2009-08-28)
changeset 3243264f30bdd3ba1
parent 32431 bcd14373ec30
child 32433 11661f4327bb
modernized messages -- eliminated ctyp/cterm operations;
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/sat_funcs.ML
src/Pure/old_goals.ML
src/Tools/induct.ML
src/ZF/Datatype_ZF.thy
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Aug 28 18:23:24 2009 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Fri Aug 28 21:04:03 2009 +0200
     1.3 @@ -531,7 +531,7 @@
     1.4  	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
     1.5  			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
     1.6  			 case opt_ty of
     1.7 -			     SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"")
     1.8 +			     SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
     1.9  			   | NONE => ())) constmaps
    1.10  	val _ = if null constmaps
    1.11  		then ()
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Aug 28 18:23:24 2009 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Aug 28 21:04:03 2009 +0200
     2.3 @@ -199,12 +199,12 @@
     2.4          val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
     2.5                             handle TERM _ => ct)
     2.6      in
     2.7 -        quote(
     2.8 +        quote (
     2.9          PrintMode.setmp [] (
    2.10          Library.setmp show_brackets false (
    2.11          Library.setmp show_all_types true (
    2.12          Library.setmp Syntax.ambiguity_is_error false (
    2.13 -        Library.setmp show_sorts true Display.string_of_cterm))))
    2.14 +        Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
    2.15          ct)
    2.16      end
    2.17  
    2.18 @@ -226,7 +226,8 @@
    2.19            | G _ = raise SMART_STRING
    2.20          fun F n =
    2.21              let
    2.22 -                val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
    2.23 +                val str =
    2.24 +                  Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
    2.25                  val u = Syntax.parse_term ctxt str
    2.26                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
    2.27              in
    2.28 @@ -234,8 +235,9 @@
    2.29                  then quote str
    2.30                  else F (n+1)
    2.31              end
    2.32 -            handle ERROR mesg => F (n+1)
    2.33 -                 | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
    2.34 +            handle ERROR mesg => F (n + 1)
    2.35 +              | SMART_STRING =>
    2.36 +                  error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
    2.37      in
    2.38        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    2.39      end
    2.40 @@ -243,8 +245,7 @@
    2.41  
    2.42  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    2.43  
    2.44 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
    2.45 -fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    2.46 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
    2.47  fun prin t = writeln (PrintMode.setmp []
    2.48    (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
    2.49  fun pth (HOLThm(ren,thm)) =
    2.50 @@ -1939,16 +1940,17 @@
    2.51                      then
    2.52                          let
    2.53                              val p1 = quotename constname
    2.54 -                            val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
    2.55 +                            val p2 = Syntax.string_of_typ_global thy'' ctype
    2.56                              val p3 = string_of_mixfix csyn
    2.57                              val p4 = smart_string_of_cterm crhs
    2.58                          in
    2.59 -                            add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
    2.60 +                          add_dump ("constdefs\n  " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n  " ^ p4) thy''
    2.61                          end
    2.62                      else
    2.63 -                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
    2.64 -                                   "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    2.65 -                                  thy'')
    2.66 +                        add_dump ("consts\n  " ^ quotename constname ^ " :: \"" ^
    2.67 +                          Syntax.string_of_typ_global thy'' ctype ^
    2.68 +                          "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n  " ^
    2.69 +                          quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
    2.70          val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
    2.71                        SOME (_,res) => HOLThm(rens_of linfo,res)
    2.72                      | NONE => raise ERR "new_definition" "Bad conclusion"
    2.73 @@ -2008,8 +2010,9 @@
    2.74                                                            in
    2.75                                                                ((cname,cT,mk_syn thy cname)::cs,p)
    2.76                                                            end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
    2.77 -                               val str = Library.foldl (fn (acc,(c,T,csyn)) =>
    2.78 -                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    2.79 +                               val str = Library.foldl (fn (acc, (c, T, csyn)) =>
    2.80 +                                   acc ^ "\n  " ^ quotename c ^ " :: \"" ^
    2.81 +                                   Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
    2.82                                 val thy' = add_dump str thy
    2.83                                 val _ = ImportRecorder.add_consts consts
    2.84                             in
    2.85 @@ -2137,7 +2140,7 @@
    2.86  fun add_dump_constdefs thy defname constname rhs ty =
    2.87      let
    2.88          val n = quotename constname
    2.89 -        val t = Display.string_of_ctyp (ctyp_of thy ty)
    2.90 +        val t = Syntax.string_of_typ_global thy ty
    2.91          val syn = string_of_mixfix (mk_syn thy constname)
    2.92          (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
    2.93          val eq = quote (constname ^ " == "^rhs)
    2.94 @@ -2224,7 +2227,7 @@
    2.95                ("  apply (rule light_ex_imp_nonempty[where t="^
    2.96                (proc_prop (cterm_of thy4 t))^"])\n"^
    2.97                ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
    2.98 -            val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
    2.99 +            val str_aty = Syntax.string_of_typ_global thy aty
   2.100              val thy = add_dump_syntax thy rep_name
   2.101              val thy = add_dump_syntax thy abs_name
   2.102              val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
     3.1 --- a/src/HOL/Import/shuffler.ML	Fri Aug 28 18:23:24 2009 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Fri Aug 28 21:04:03 2009 +0200
     3.3 @@ -57,7 +57,6 @@
     3.4  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     3.5  
     3.6  val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
     3.7 -val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
     3.8  
     3.9  fun mk_meta_eq th =
    3.10      (case concl_of th of
    3.11 @@ -304,13 +303,14 @@
    3.12                  val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    3.13              in
    3.14                  if not (lhs aconv origt)
    3.15 -                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    3.16 -                      writeln (Display.string_of_cterm (cterm_of thy origt));
    3.17 -                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    3.18 -                      writeln (Display.string_of_cterm (cterm_of thy typet));
    3.19 -                      writeln (Display.string_of_cterm (cterm_of thy t));
    3.20 -                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    3.21 -                      writeln "done")
    3.22 +                then
    3.23 +                  writeln (cat_lines
    3.24 +                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
    3.25 +                      Syntax.string_of_term_global thy origt,
    3.26 +                      Syntax.string_of_term_global thy lhs,
    3.27 +                      Syntax.string_of_term_global thy typet,
    3.28 +                      Syntax.string_of_term_global thy t] @
    3.29 +                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
    3.30                  else ()
    3.31              end
    3.32      in
    3.33 @@ -366,13 +366,14 @@
    3.34                  val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    3.35              in
    3.36                  if not (lhs aconv origt)
    3.37 -                then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    3.38 -                      writeln (Display.string_of_cterm (cterm_of thy origt));
    3.39 -                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    3.40 -                      writeln (Display.string_of_cterm (cterm_of thy typet));
    3.41 -                      writeln (Display.string_of_cterm (cterm_of thy t));
    3.42 -                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    3.43 -                      writeln "done")
    3.44 +                then
    3.45 +                  writeln (cat_lines
    3.46 +                    (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
    3.47 +                      Syntax.string_of_term_global thy origt,
    3.48 +                      Syntax.string_of_term_global thy lhs,
    3.49 +                      Syntax.string_of_term_global thy typet,
    3.50 +                      Syntax.string_of_term_global thy t] @
    3.51 +                      map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
    3.52                  else ()
    3.53              end
    3.54      in
    3.55 @@ -407,9 +408,8 @@
    3.56                        end
    3.57                      | _ => NONE)
    3.58              else NONE
    3.59 -          | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
    3.60 -    end
    3.61 -    handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
    3.62 +          | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
    3.63 +    end;
    3.64  
    3.65  fun mk_tfree s = TFree("'"^s,[])
    3.66  fun mk_free s t = Free (s,t)
     4.1 --- a/src/HOL/Statespace/state_space.ML	Fri Aug 28 18:23:24 2009 +0200
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Aug 28 21:04:03 2009 +0200
     4.3 @@ -567,8 +567,8 @@
     4.4            (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
     4.5               []  => []
     4.6             | [_] => []
     4.7 -           | rs  => ["Different types for component " ^ n ^": " ^ commas
     4.8 -                       (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
     4.9 +           | rs  => ["Different types for component " ^ n ^": " ^
    4.10 +                commas (map (Syntax.string_of_typ ctxt o snd) rs)])
    4.11  
    4.12      val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
    4.13  
     5.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Aug 28 18:23:24 2009 +0200
     5.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Fri Aug 28 21:04:03 2009 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  sig
     5.5    val trace: bool ref
     5.6    val trace_thms: string -> thm list -> unit
     5.7 -  val trace_cterms: string -> cterm list -> unit
     5.8 +  val trace_cterm: string -> cterm -> unit
     5.9    type pattern
    5.10    val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    5.11    val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    5.12 @@ -296,7 +296,7 @@
    5.13              raise TFL_ERR "no_repeat_vars"
    5.14                            (quote (#1 (dest_Free v)) ^
    5.15                            " occurs repeatedly in the pattern " ^
    5.16 -                          quote (Display.string_of_cterm (Thry.typecheck thy pat)))
    5.17 +                          quote (Syntax.string_of_term_global thy pat))
    5.18           else check rst
    5.19   in check (FV_multiset pat)
    5.20   end;
    5.21 @@ -912,9 +912,10 @@
    5.22    if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
    5.23    else ();
    5.24  
    5.25 -fun trace_cterms s L =
    5.26 -  if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
    5.27 -  else ();;
    5.28 +fun trace_cterm s ct =
    5.29 +  if !trace then
    5.30 +    writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
    5.31 +  else ();
    5.32  
    5.33  
    5.34  fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    5.35 @@ -942,7 +943,7 @@
    5.36  
    5.37     fun simplify_tc tc (r,ind) =
    5.38         let val tc1 = tych tc
    5.39 -           val _ = trace_cterms "TC before simplification: " [tc1]
    5.40 +           val _ = trace_cterm "TC before simplification: " tc1
    5.41             val tc_eq = simplifier tc1
    5.42             val _ = trace_thms "result: " [tc_eq]
    5.43         in
     6.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Aug 28 18:23:24 2009 +0200
     6.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Aug 28 21:04:03 2009 +0200
     6.3 @@ -299,7 +299,7 @@
     6.4    (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
     6.5       them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
     6.6       that new TVars are distinct and that types can be inferred from terms.*)
     6.7 -  fun inst_inf ctxt thpairs fsubst th =    
     6.8 +  fun inst_inf ctxt thpairs fsubst th =
     6.9      let val thy = ProofContext.theory_of ctxt
    6.10          val i_th   = lookth thpairs th
    6.11          val i_th_vars = Term.add_vars (prop_of i_th) []
    6.12 @@ -324,11 +324,12 @@
    6.13          val tms = infer_types ctxt rawtms;
    6.14          val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
    6.15          val substs' = ListPair.zip (vars, map ctm_of tms)
    6.16 -        val _ = Output.debug (fn() => "subst_translations:")
    6.17 -        val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
    6.18 -                                                        Display.string_of_cterm y))
    6.19 -                  substs'
    6.20 -    in  cterm_instantiate substs' i_th  
    6.21 +        val _ = Output.debug (fn () =>
    6.22 +          cat_lines ("subst_translations:" ::
    6.23 +            (substs' |> map (fn (x, y) =>
    6.24 +              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
    6.25 +              Syntax.string_of_term ctxt (term_of y)))));
    6.26 +    in  cterm_instantiate substs' i_th
    6.27          handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
    6.28      end;
    6.29  
    6.30 @@ -610,14 +611,14 @@
    6.31                    if null unused then ()
    6.32                    else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
    6.33                    case result of
    6.34 -                      (_,ith)::_ => 
    6.35 -                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
    6.36 +                      (_,ith)::_ =>
    6.37 +                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
    6.38                             [ith])
    6.39 -                    | _ => (Output.debug (fn () => "Metis: no result"); 
    6.40 +                    | _ => (Output.debug (fn () => "Metis: no result");
    6.41                              [])
    6.42                end
    6.43 -          | Metis.Resolution.Satisfiable _ => 
    6.44 -	      (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied"); 
    6.45 +          | Metis.Resolution.Satisfiable _ =>
    6.46 +	      (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
    6.47  	       [])
    6.48      end;
    6.49  
    6.50 @@ -625,9 +626,9 @@
    6.51      let val _ = Output.debug (fn () =>
    6.52            "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    6.53      in
    6.54 -       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
    6.55 +       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
    6.56         then (warning "Proof state contains the empty sort"; Seq.empty)
    6.57 -       else 
    6.58 +       else
    6.59  	 (Meson.MESON ResAxioms.neg_clausify
    6.60  	   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
    6.61  	  THEN ResAxioms.expand_defs_tac st0) st0
     7.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri Aug 28 18:23:24 2009 +0200
     7.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri Aug 28 21:04:03 2009 +0200
     7.3 @@ -51,7 +51,7 @@
     7.4  	val trace_sat: bool ref    (* input: print trace messages *)
     7.5  	val solver: string ref  (* input: name of SAT solver to be used *)
     7.6  	val counter: int ref     (* output: number of resolution steps during last proof replay *)
     7.7 -	val rawsat_thm: cterm list -> thm
     7.8 +	val rawsat_thm: Proof.context -> cterm list -> thm
     7.9  	val rawsat_tac: Proof.context -> int -> tactic
    7.10  	val sat_tac: Proof.context -> int -> tactic
    7.11  	val satx_tac: Proof.context -> int -> tactic
    7.12 @@ -295,9 +295,7 @@
    7.13  (*      hyps).                                                               *)
    7.14  (* ------------------------------------------------------------------------- *)
    7.15  
    7.16 -(* Thm.cterm list -> Thm.thm *)
    7.17 -
    7.18 -fun rawsat_thm clauses =
    7.19 +fun rawsat_thm ctxt clauses =
    7.20  let
    7.21  	(* remove premises that equal "True" *)
    7.22  	val clauses' = filter (fn clause =>
    7.23 @@ -310,7 +308,7 @@
    7.24  		((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
    7.25  			handle TERM ("dest_Trueprop", _) => false)
    7.26  		orelse (
    7.27 -			warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
    7.28 +			warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
    7.29  			false)) clauses'
    7.30  	(* remove trivial clauses -- this is necessary because zChaff removes *)
    7.31  	(* trivial clauses during preprocessing, and otherwise our clause     *)
    7.32 @@ -323,7 +321,8 @@
    7.33  	(* sorted in ascending order                                          *)
    7.34  	val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
    7.35  	val _ = if !trace_sat then
    7.36 -			tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
    7.37 +			tracing ("Sorted non-trivial clauses:\n" ^
    7.38 +			  cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
    7.39  		else ()
    7.40  	(* translate clauses from HOL terms to PropLogic.prop_formula *)
    7.41  	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
    7.42 @@ -411,7 +410,8 @@
    7.43  (* ------------------------------------------------------------------------- *)
    7.44  
    7.45  fun rawsat_tac ctxt i =
    7.46 -  Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
    7.47 +  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
    7.48 +    rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
    7.49  
    7.50  (* ------------------------------------------------------------------------- *)
    7.51  (* pre_cnf_tac: converts the i-th subgoal                                    *)
     8.1 --- a/src/Pure/old_goals.ML	Fri Aug 28 18:23:24 2009 +0200
     8.2 +++ b/src/Pure/old_goals.ML	Fri Aug 28 21:04:03 2009 +0200
     8.3 @@ -362,10 +362,7 @@
     8.4            (case Seq.pull (tac st0) of
     8.5                 SOME(st,_) => st
     8.6               | _ => error ("prove_goal: tactic failed"))
     8.7 -  in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
     8.8 -  handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
     8.9 -               writeln ("The exception above was raised for\n" ^
    8.10 -                      Display.string_of_cterm chorn); raise e);
    8.11 +  in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end;
    8.12  
    8.13  (*Two variants: one checking the result, one not.
    8.14    Neither prints runtime messages: they are for internal packages.*)
     9.1 --- a/src/Tools/induct.ML	Fri Aug 28 18:23:24 2009 +0200
     9.2 +++ b/src/Tools/induct.ML	Fri Aug 28 21:04:03 2009 +0200
     9.3 @@ -288,21 +288,21 @@
     9.4  
     9.5  (* prep_inst *)
     9.6  
     9.7 -fun prep_inst thy align tune (tm, ts) =
     9.8 +fun prep_inst ctxt align tune (tm, ts) =
     9.9    let
    9.10 -    val cert = Thm.cterm_of thy;
    9.11 +    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    9.12      fun prep_var (x, SOME t) =
    9.13            let
    9.14              val cx = cert x;
    9.15              val xT = #T (Thm.rep_cterm cx);
    9.16              val ct = cert (tune t);
    9.17 -            val tT = Thm.ctyp_of_term ct;
    9.18 +            val tT = #T (Thm.rep_cterm ct);
    9.19            in
    9.20 -            if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
    9.21 +            if Type.could_unify (tT, xT) then SOME (cx, ct)
    9.22              else error (Pretty.string_of (Pretty.block
    9.23               [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
    9.24 -              Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
    9.25 -              Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
    9.26 +              Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
    9.27 +              Syntax.pretty_typ ctxt tT]))
    9.28            end
    9.29        | prep_var (_, NONE) = NONE;
    9.30      val xs = vars_of tm;
    9.31 @@ -342,12 +342,11 @@
    9.32  fun cases_tac ctxt insts opt_rule facts =
    9.33    let
    9.34      val thy = ProofContext.theory_of ctxt;
    9.35 -    val cert = Thm.cterm_of thy;
    9.36  
    9.37      fun inst_rule r =
    9.38        if null insts then `RuleCases.get r
    9.39        else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    9.40 -        |> maps (prep_inst thy align_left I)
    9.41 +        |> maps (prep_inst ctxt align_left I)
    9.42          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
    9.43  
    9.44      val ruleq =
    9.45 @@ -411,8 +410,8 @@
    9.46  
    9.47  (* prepare rule *)
    9.48  
    9.49 -fun rule_instance thy inst rule =
    9.50 -  Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
    9.51 +fun rule_instance ctxt inst rule =
    9.52 +  Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
    9.53  
    9.54  fun internalize k th =
    9.55    th |> Thm.permute_prems 0 k
    9.56 @@ -589,7 +588,7 @@
    9.57        (if null insts then `RuleCases.get r
    9.58         else (align_left "Rule has fewer conclusions than arguments given"
    9.59            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    9.60 -        |> maps (prep_inst thy align_right (atomize_term thy))
    9.61 +        |> maps (prep_inst ctxt align_right (atomize_term thy))
    9.62          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
    9.63        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    9.64  
    9.65 @@ -619,7 +618,7 @@
    9.66            THEN' inner_atomize_tac) j))
    9.67          THEN' atomize_tac) i st |> Seq.maps (fn st' =>
    9.68              guess_instance ctxt (internalize more_consumes rule) i st'
    9.69 -            |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    9.70 +            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    9.71              |> Seq.maps (fn rule' =>
    9.72                CASES (rule_cases rule' cases)
    9.73                  (Tactic.rtac rule' i THEN
    9.74 @@ -657,7 +656,7 @@
    9.75  
    9.76      fun inst_rule r =
    9.77        if null inst then `RuleCases.get r
    9.78 -      else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
    9.79 +      else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
    9.80          |> pair (RuleCases.get r);
    9.81  
    9.82      fun ruleq goal =
    9.83 @@ -673,7 +672,7 @@
    9.84        |> Seq.maps (RuleCases.consume [] facts)
    9.85        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    9.86          guess_instance ctxt rule i st
    9.87 -        |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
    9.88 +        |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    9.89          |> Seq.maps (fn rule' =>
    9.90            CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
    9.91              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
    10.1 --- a/src/ZF/Datatype_ZF.thy	Fri Aug 28 18:23:24 2009 +0200
    10.2 +++ b/src/ZF/Datatype_ZF.thy	Fri Aug 28 21:04:03 2009 +0200
    10.3 @@ -14,9 +14,9 @@
    10.4  (*Typechecking rules for most datatypes involving univ*)
    10.5  structure Data_Arg =
    10.6    struct
    10.7 -  val intrs = 
    10.8 +  val intrs =
    10.9        [@{thm SigmaI}, @{thm InlI}, @{thm InrI},
   10.10 -       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ}, 
   10.11 +       @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
   10.12         @{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
   10.13  
   10.14  
   10.15 @@ -25,7 +25,7 @@
   10.16    end;
   10.17  
   10.18  
   10.19 -structure Data_Package = 
   10.20 +structure Data_Package =
   10.21    Add_datatype_def_Fun
   10.22     (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
   10.23      and Su=Standard_Sum
   10.24 @@ -37,16 +37,16 @@
   10.25  (*Typechecking rules for most codatatypes involving quniv*)
   10.26  structure CoData_Arg =
   10.27    struct
   10.28 -  val intrs = 
   10.29 +  val intrs =
   10.30        [@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
   10.31 -       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv}, 
   10.32 +       @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
   10.33         @{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
   10.34  
   10.35    val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD},   (*for mutual recursion*)
   10.36                 @{thm QSigmaE}, @{thm qsumE}];                    (*allows * and + in spec*)
   10.37    end;
   10.38  
   10.39 -structure CoData_Package = 
   10.40 +structure CoData_Package =
   10.41    Add_datatype_def_Fun
   10.42     (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
   10.43      and Su=Quine_Sum
   10.44 @@ -69,9 +69,9 @@
   10.45   val datatype_ss = @{simpset};
   10.46  
   10.47   fun proc sg ss old =
   10.48 -   let val _ = if !trace then writeln ("data_free: OLD = " ^ 
   10.49 -                                       Display.string_of_cterm (cterm_of sg old))
   10.50 -               else ()
   10.51 +   let val _ =
   10.52 +         if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
   10.53 +         else ()
   10.54         val (lhs,rhs) = FOLogic.dest_eq old
   10.55         val (lhead, largs) = strip_comb lhs
   10.56         and (rhead, rargs) = strip_comb rhs
   10.57 @@ -81,15 +81,15 @@
   10.58           handle Option => raise Match;
   10.59         val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
   10.60           handle Option => raise Match;
   10.61 -       val new = 
   10.62 -           if #big_rec_name lcon_info = #big_rec_name rcon_info 
   10.63 +       val new =
   10.64 +           if #big_rec_name lcon_info = #big_rec_name rcon_info
   10.65                 andalso not (null (#free_iffs lcon_info)) then
   10.66                 if lname = rname then mk_new (largs, rargs)
   10.67                 else Const("False",FOLogic.oT)
   10.68             else raise Match
   10.69 -       val _ = if !trace then 
   10.70 -                 writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
   10.71 -               else ();
   10.72 +       val _ =
   10.73 +         if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
   10.74 +         else ();
   10.75         val goal = Logic.mk_equals (old, new)
   10.76         val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
   10.77           (fn _ => rtac iff_reflection 1 THEN