# HG changeset patch # User wenzelm # Date 1119025993 -7200 # Node ID d2203a276b0791d90be79f5a4f98ae50c9ad3ca7 # Parent 9975aab75d72d3cd5d536b9f45dea4ecec27acb7 accomodate change of TheoryDataFun; Context.str_of_thy; diff -r 9975aab75d72 -r d2203a276b07 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Fri Jun 17 18:33:12 2005 +0200 +++ b/src/HOL/Import/shuffler.ML Fri Jun 17 18:33:13 2005 +0200 @@ -45,7 +45,7 @@ List.app print_thm thms) | THEORY (msg,thys) => (writeln ("Exception THEORY raised:\n" ^ msg); - List.app (Pretty.writeln o Display.pretty_theory) thys) + List.app (writeln o Context.str_of_thy) thys) | TERM (msg,ts) => (writeln ("Exception TERM raised:\n" ^ msg); List.app (writeln o Sign.string_of_term sign) ts) @@ -81,8 +81,8 @@ type T = thm list val empty = [] val copy = I -val prep_ext = I -val merge = Library.gen_union Thm.eq_thm +val extend = I +fun merge _ = Library.gen_union Thm.eq_thm fun print sg thms = Pretty.writeln (Pretty.big_list "Shuffle theorems:" (map Display.pretty_thm thms)) @@ -477,7 +477,7 @@ val norms = ShuffleData.get thy val ss = empty_ss setmksimps single - addsimps (map (transfer_sg sg) norms) + addsimps (map (Thm.transfer sg) norms) fun chain f th = let val rhs = snd (dest_equals (cprop_of th)) @@ -581,7 +581,7 @@ fun process [] = NONE | process ((name,th)::thms) = let - val norm_th = varifyT (norm_thm thy (close_thm (transfer_sg sg th))) + val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th))) val triv_th = trivial rhs val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of