src/Pure/tactic.ML
changeset 11974 f76c3e1ab352
parent 11970 e7eedbd2c8ca
child 12139 d51d50636332
     1.1 --- a/src/Pure/tactic.ML	Sat Oct 27 23:21:19 2001 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sun Oct 28 19:44:26 2001 +0100
     1.3 @@ -618,7 +618,6 @@
     1.4      val frees = map Term.dest_Free (Term.term_frees statement);
     1.5      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
     1.6      val fixed_tfrees = foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
     1.7 -
     1.8      val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
     1.9  
    1.10      fun err msg = error (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
    1.11 @@ -628,8 +627,9 @@
    1.12        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.13  
    1.14      val _ = cert_safe statement;
    1.15 -    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => error msg;
    1.16 +    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
    1.17  
    1.18 +    val cparams = map (cert_safe o Free) params;
    1.19      val casms = map cert_safe asms;
    1.20      val prems = map (norm_hhf o Thm.assume) casms;
    1.21      val goal = Drule.mk_triv_goal (cert_safe prop);
    1.22 @@ -648,7 +648,7 @@
    1.23      else
    1.24        raw_result
    1.25        |> Drule.implies_intr_list casms
    1.26 -      |> Drule.forall_intr_list (map (cert_safe o Free) params)
    1.27 +      |> Drule.forall_intr_list cparams
    1.28        |> norm_hhf
    1.29        |> Thm.varifyT' fixed_tfrees
    1.30        |> Drule.zero_var_indexes