src/HOL/Tools/TFL/rules.ML

 
 
 (*---------------------------------------------------------------------------
  * Trace information for the rewriter
  *---------------------------------------------------------------------------*)
-val term_ref = ref[] : term list ref
+val term_ref = ref [] : term list ref
 val ss_ref = ref [] : simpset list ref;
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
 
 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_cterms s L =
-  say (cat_lines (s :: map Display.string_of_cterm L));
+fun print_cterm s ct =
+  say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
 
 
 (*---------------------------------------------------------------------------
  * General abstraction handlers, should probably go in USyntax.
  *---------------------------------------------------------------------------*)

              val dummy = thm_ref := (thm :: !thm_ref)
              val dummy = ss_ref := (ss :: !ss_ref)
              (* Unquantified eliminate *)
              fun uq_eliminate (thm,imp,thy) =
                  let val tych = cterm_of thy
-                     val dummy = print_cterms "To eliminate:" [tych imp]
+                     val dummy = print_cterm "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 ss' = Simplifier.add_prems (map ASSUME ants) ss
                      val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs

               val rcontext = rev cntxt
               val cncl = HOLogic.dest_Trueprop o Thm.prop_of
               val antl = case rcontext of [] => []
                          | _   => [S.list_mk_conj(map cncl rcontext)]
               val TC = genl(S.list_mk_imp(antl, A))
-              val dummy = print_cterms "func:" [cterm_of thy func]
-              val dummy = print_cterms "TC:"
-                              [cterm_of thy (HOLogic.mk_Trueprop TC)]
+              val dummy = print_cterm "func:" (cterm_of thy func)
+              val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
               val dummy = tc_list := (TC :: !tc_list)
               val nestedp = isSome (S.find_term is_func TC)
               val dummy = if nestedp then say "nested" else say "not_nested"
               val dummy = term_ref := ([func,TC]@(!term_ref))
               val th' = if nestedp then raise RULES_ERR "solver" "nested function"