Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Import/import.ML
changeset 32091 30e2ffbba718
parent 31945 d5f186aa0bed
child 32740 9dd0a2f83429 
     1.1 --- a/src/HOL/Import/import.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/HOL/Import/import.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -44,9 +44,9 @@
     1.4              val thm = equal_elim rew thm
     1.5              val prew = ProofKernel.rewrite_hol4_term prem thy
     1.6              val prem' = #2 (Logic.dest_equals (prop_of prew))
     1.7 -            val _ = message ("Import proved " ^ Display.string_of_thm thm)
     1.8 +            val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
     1.9              val thm = ProofKernel.disambiguate_frees thm
    1.10 -            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
    1.11 +            val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
    1.12          in
    1.13              case Shuffler.set_prop thy prem' [("",thm)] of
    1.14                  SOME (_,thm) =>
isabelle