src/HOL/HOL.ML
changeset 5346 bc9748ad8491
parent 5309 01c2b317da88
child 5447 df03d330aeab
equal deleted inserted replaced
5345:d7927fc7170d 5346:bc9748ad8491
   391   (case concl_of th of
   391   (case concl_of th of
   392      _ $ (Const("op -->",_)$_$_) => th RS mp
   392      _ $ (Const("op -->",_)$_$_) => th RS mp
   393   | _ => raise THM("RSmp",0,[th]));
   393   | _ => raise THM("RSmp",0,[th]));
   394 
   394 
   395 fun normalize_thm funs =
   395 fun normalize_thm funs =
   396 let fun trans [] th = th
   396   let fun trans [] th = th
   397       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   397 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   398 in trans funs end;
   398   in zero_var_indexes o trans funs end;
   399 
   399 
   400 fun qed_spec_mp name =
   400 fun qed_spec_mp name =
   401   let val thm = normalize_thm [RSspec,RSmp] (result())
   401   let val thm = normalize_thm [RSspec,RSmp] (result())
   402   in bind_thm(name, thm) end;
   402   in ml_store_thm(name, thm) end;
   403 
   403 
   404 fun qed_goal_spec_mp name thy s p = 
   404 fun qed_goal_spec_mp name thy s p = 
   405 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   405 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   406 
   406 
   407 fun qed_goalw_spec_mp name thy defs s p = 
   407 fun qed_goalw_spec_mp name thy defs s p =