src/FOLP/simp.ML
changeset 611 11098f505bfe
parent 231 cb6a24451544
child 1459 d12da312eff4
equal deleted inserted replaced
610:ede55dd46f9d 611:11098f505bfe
   588      None => []  |  Some(refl) => [mk_cong sg (f,aTs,rT) refl]
   588      None => []  |  Some(refl) => [mk_cong sg (f,aTs,rT) refl]
   589 end;
   589 end;
   590 
   590 
   591 fun mk_cong_thy thy f =
   591 fun mk_cong_thy thy f =
   592 let val sg = sign_of thy;
   592 let val sg = sign_of thy;
   593     val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
   593     val T = case Sign.const_type sg f of
   594 		None => error(f^" not declared") | Some(T) => T;
   594 		None => error(f^" not declared") | Some(T) => T;
   595     val T' = incr_tvar 9 T;
   595     val T' = incr_tvar 9 T;
   596 in mk_cong_type sg (Const(f,T'),T') end;
   596 in mk_cong_type sg (Const(f,T'),T') end;
   597 
   597 
   598 fun mk_congs thy = flat o map (mk_cong_thy thy);
   598 fun mk_congs thy = flat o map (mk_cong_thy thy);
   600 fun mk_typed_congs thy =
   600 fun mk_typed_congs thy =
   601 let val sg = sign_of thy;
   601 let val sg = sign_of thy;
   602     val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
   602     val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
   603     fun readfT(f,s) =
   603     fun readfT(f,s) =
   604 	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
   604 	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
   605 	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
   605 	    val t = case Sign.const_type sg f of
   606 		      Some(_) => Const(f,T) | None => Free(f,T)
   606 		      Some(_) => Const(f,T) | None => Free(f,T)
   607 	in (t,T) end
   607 	in (t,T) end
   608 in flat o map (mk_cong_type sg o readfT) end;
   608 in flat o map (mk_cong_type sg o readfT) end;
   609 
   609 
   610 end (* local *)
   610 end (* local *)