accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:33:13 2005 +0200 (2005-06-17)
changeset 16428d2203a276b07
parent 16427 9975aab75d72
child 16429 e871f4b1a4f0
accomodate change of TheoryDataFun;
Context.str_of_thy;
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Jun 17 18:33:12 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Fri Jun 17 18:33:13 2005 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  	  List.app print_thm thms)
     1.5     | THEORY (msg,thys) =>
     1.6  	 (writeln ("Exception THEORY raised:\n" ^ msg);
     1.7 -	  List.app (Pretty.writeln o Display.pretty_theory) thys)
     1.8 +	  List.app (writeln o Context.str_of_thy) thys)
     1.9     | TERM (msg,ts) =>
    1.10  	 (writeln ("Exception TERM raised:\n" ^ msg);
    1.11  	  List.app (writeln o Sign.string_of_term sign) ts)
    1.12 @@ -81,8 +81,8 @@
    1.13  type T = thm list
    1.14  val empty = []
    1.15  val copy = I
    1.16 -val prep_ext = I
    1.17 -val merge = Library.gen_union Thm.eq_thm
    1.18 +val extend = I
    1.19 +fun merge _ = Library.gen_union Thm.eq_thm
    1.20  fun print sg thms =
    1.21      Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    1.22  				    (map Display.pretty_thm thms))
    1.23 @@ -477,7 +477,7 @@
    1.24  
    1.25  	val norms = ShuffleData.get thy
    1.26  	val ss = empty_ss setmksimps single
    1.27 -			  addsimps (map (transfer_sg sg) norms)
    1.28 +			  addsimps (map (Thm.transfer sg) norms)
    1.29  	fun chain f th =
    1.30  	    let
    1.31  		val rhs = snd (dest_equals (cprop_of th))
    1.32 @@ -581,7 +581,7 @@
    1.33  	fun process [] = NONE
    1.34  	  | process ((name,th)::thms) =
    1.35  	    let
    1.36 -		val norm_th = varifyT (norm_thm thy (close_thm (transfer_sg sg th)))
    1.37 +		val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
    1.38  		val triv_th = trivial rhs
    1.39  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
    1.40  		val mod_th = case Seq.pull (bicompose true (false,norm_th,0) 1 triv_th) of