1.1 --- a/src/Tools/isac/Specify/refine.sml	Sat Aug 26 11:37:16 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Sat Aug 26 15:14:24 2023 +0200
     1.3 @@ -223,6 +223,9 @@
     1.4  );
     1.5  
     1.6  \<^isac_test>\<open>
     1.7 +(**)
     1.8 +\<close>
     1.9 +
    1.10  (* refine a problem; version providing output for math authors *)
    1.11  (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list -> 
    1.12      Probl_Def.T Store.node -> M_Match.T list*)
    1.13 @@ -266,7 +269,6 @@
    1.14          M_Match.Matches _ => pbls'
    1.15        | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
    1.16      end;
    1.17 -\<close>
    1.18  
    1.19  (*
    1.20    TODO: rename \<rightarrow> apply_to_node
    1.21 @@ -289,10 +291,11 @@
    1.22  	  | NONE => NONE
    1.23  	end;
    1.24  fun refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;
    1.25 +fun xxxxx ctxt fmz pblID =
    1.26 +  app_ptyp (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);
    1.27  
    1.28  \<^isac_test>\<open>
    1.29 -fun xxxxx ctxt fmz pblID =
    1.30 -  app_ptyp (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);
    1.31 +(**)
    1.32  \<close>
    1.33  
    1.34  (**)end(**)