# HG changeset patch # User wenzelm # Date 1729001497 -7200 # Node ID 98fd5375de00100949d374a79c6b5c7532ab7157 # Parent 2d73c3287bd3ea27d81d482d40fa3ecb401182ad minor performance tuning; diff -r 2d73c3287bd3 -r 98fd5375de00 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Oct 15 14:57:23 2024 +0200 +++ b/src/Pure/Syntax/ast.ML Tue Oct 15 16:11:37 2024 +0200 @@ -200,13 +200,13 @@ | subst env (Variable x) = the (Symtab.lookup env x) | subst env (Appl asts) = Appl (map (subst env) asts); -fun head_name (Constant a) = SOME a - | head_name (Variable a) = SOME a - | head_name (Appl [Constant "_constrain", Constant a, _]) = SOME a - | head_name (Appl (Appl [Constant "_constrain", Constant a, _] :: _)) = SOME a - | head_name (Appl (Constant a :: _)) = SOME a - | head_name (Appl (Variable a :: _)) = SOME a - | head_name _ = NONE; +fun head_name (Constant a) = a + | head_name (Variable a) = a + | head_name (Appl [Constant "_constrain", Constant a, _]) = a + | head_name (Appl (Appl [Constant "_constrain", Constant a, _] :: _)) = a + | head_name (Appl (Constant a :: _)) = a + | head_name (Appl (Variable a :: _)) = a + | head_name _ = ""; fun message head body = Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); @@ -230,11 +230,10 @@ | NONE => (Unsynchronized.inc failed_matches; rewrite1 pats ast)) | rewrite1 [] _ = NONE; - fun rewrite2 (SOME a) ast = - (case rewrite1 (get_rules a) ast of - NONE => rewrite2 NONE ast - | some => some) - | rewrite2 NONE ast = rewrite1 (get_rules "") ast; + fun rewrite2 a ast = + (case rewrite1 (get_rules a) ast of + NONE => if a = "" then NONE else rewrite2 "" ast + | some => some); fun rewrite ast = rewrite2 (head_name ast) ast;