Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
authorwenzelm
Fri, 28 Oct 2005 22:27:56 +0200
changeset 18028 99a307bdfe15
parent 18027 09ab79d4e8e1
child 18029 19f1ad18bece
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
src/Pure/goals.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/goals.ML	Fri Oct 28 22:27:55 2005 +0200
+++ b/src/Pure/goals.ML	Fri Oct 28 22:27:56 2005 +0200
@@ -381,7 +381,7 @@
     val _ = warn_obsolete ();
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
-    val asms = map (Goal.norm_hhf_rule o assume) As;
+    val asms = map (Goal.norm_hhf o Thm.assume) As;
     fun check NONE = error "prove_goal: tactic failed"
       | check (SOME (thm, _)) = (case nprems_of thm of
             0 => thm
isabelle