1.1 --- a/src/Tools/isac/Knowledge/InsSort.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  (*-------------------------from InsSort.ML 8.3.01----------------------*)
     1.6  
     1.7 -theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
     1.8 +theory' := (!theory') @ [("InsSort",InsSort.thy)];
     1.9  
    1.10  val ins_sort = 
    1.11    Rls{preconds = [], rew_ord = ("tless_true",tless_true),
    1.12 @@ -42,13 +42,13 @@
    1.13  
    1.14  
    1.15  (* 
    1.16 -> get_pbt ["Script.thy","squareroot","univariate","equation"];
    1.17 -> get_met ("Script.thy","max_on_interval_by_calculus");
    1.18 +> get_pbt ["Script","squareroot","univariate","equation"];
    1.19 +> get_met ("Script","max_on_interval_by_calculus");
    1.20  *)
    1.21  pbltypes:= (!pbltypes) @ 
    1.22  [
    1.23   prep_pbt InsSort.thy
    1.24 - (["InsSort.thy","inssort"]:pblID,
    1.25 + (["InsSort","inssort"]:pblID,
    1.26    [("#Given" ,"unsorted u_"),
    1.27     ("#Find"  ,"sorted s_")
    1.28    ])
    1.29 @@ -57,13 +57,13 @@
    1.30  methods:= (!methods) @
    1.31  [
    1.32  (*, -------17.6.00,
    1.33 - (("InsSort.thy","inssort"):metID,
    1.34 + (("InsSort","inssort"):metID,
    1.35    {ppc = prep_met
    1.36     [("#Given" ,"unsorted u_"),
    1.37      ("#Find"  ,"sorted s_")
    1.38      ],
    1.39     rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
    1.40 -   scr=Script (((inst_abs (assoc_thm "InsSort.thy")) 
    1.41 +   scr=Script (((inst_abs (assoc_thm "InsSort")) 
    1.42                o term_of o the o (parse thy))    (*for [#1,#3,#2] only*)
    1.43        "Script Ins_sort (u_::'a list) =          \
    1.44         \ (let u_ = Rewrite sort_def   False u_; \
    1.45 @@ -85,7 +85,7 @@
    1.46         \  in u_)")
    1.47    } : met),
    1.48  
    1.49 - (("InsSort.thy","sort"):metID,
    1.50 + (("InsSort","sort"):metID,
    1.51    {ppc = prep_met
    1.52     [("#Given" ,"unsorted u_"),
    1.53      ("#Find"  ,"sorted s_")