diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/InsSort.sml
--- a/src/Tools/isac/Knowledge/InsSort.sml	Wed Sep 08 16:45:27 2010 +0200
+++ b/src/Tools/isac/Knowledge/InsSort.sml	Wed Sep 08 16:47:22 2010 +0200
@@ -20,7 +20,7 @@
 
 (*-------------------------from InsSort.ML 8.3.01----------------------*)
 
-theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
+theory' := (!theory') @ [("InsSort",InsSort.thy)];
 
 val ins_sort = 
   Rls{preconds = [], rew_ord = ("tless_true",tless_true),
@@ -42,13 +42,13 @@
 
 
 (* 
-> get_pbt ["Script.thy","squareroot","univariate","equation"];
-> get_met ("Script.thy","max_on_interval_by_calculus");
+> get_pbt ["Script","squareroot","univariate","equation"];
+> get_met ("Script","max_on_interval_by_calculus");
 *)
 pbltypes:= (!pbltypes) @ 
 [
  prep_pbt InsSort.thy
- (["InsSort.thy","inssort"]:pblID,
+ (["InsSort","inssort"]:pblID,
   [("#Given" ,"unsorted u_"),
    ("#Find"  ,"sorted s_")
   ])
@@ -57,13 +57,13 @@
 methods:= (!methods) @
 [
 (*, -------17.6.00,
- (("InsSort.thy","inssort"):metID,
+ (("InsSort","inssort"):metID,
   {ppc = prep_met
    [("#Given" ,"unsorted u_"),
     ("#Find"  ,"sorted s_")
     ],
    rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
-   scr=Script (((inst_abs (assoc_thm "InsSort.thy")) 
+   scr=Script (((inst_abs (assoc_thm "InsSort")) 
               o term_of o the o (parse thy))    (*for [#1,#3,#2] only*)
       "Script Ins_sort (u_::'a list) =          \
        \ (let u_ = Rewrite sort_def   False u_; \
@@ -85,7 +85,7 @@
        \  in u_)")
   } : met),
 
- (("InsSort.thy","sort"):metID,
+ (("InsSort","sort"):metID,
   {ppc = prep_met
    [("#Given" ,"unsorted u_"),
     ("#Find"  ,"sorted s_")