Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/splitter.ML
changeset 82661 8a02dd7fcb5d
parent 80664 477ca08c9091 
--- a/src/Provers/splitter.ML	Wed May 21 22:03:53 2025 +0200
+++ b/src/Provers/splitter.ML	Wed May 21 20:44:12 2025 +0200
@@ -438,7 +438,7 @@
 fun split_name (name, T) asm = "split " ^
   (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
 
-fun gen_add_split bang split ctxt =
+fun gen_add_split bang split =
   let
     val (name, asm) = split_thm_info split
     val split0 = Thm.trim_context split
@@ -450,14 +450,14 @@
                    TRY o (SELECT_GOAL (Data.safe_tac ctxt'))
               else split_tac ctxt' [split'])
       end
-  in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
+  in Simplifier.add_loop (split_name name asm, tac) end;
 
 val add_split = gen_add_split false;
 val add_split_bang = gen_add_split true;
 
-fun del_split split ctxt =
+fun del_split split =
   let val (name, asm) = split_thm_info split
-  in Simplifier.delloop (ctxt, split_name name asm) end;
+  in Simplifier.del_loop (split_name name asm) end;
 
 
 (* attributes *)
isabelle