Nominal-General/nominal_eqvt.ML
changeset 2117 b3a5bda07007
parent 2110 872187804ff5
child 2168 ce0255ffaeb4
equal deleted inserted replaced
2110:872187804ff5 2117:b3a5bda07007
   147   (thm', ctxt')
   147   (thm', ctxt')
   148 end
   148 end
   149 
   149 
   150 fun equivariance pred_trms raw_induct intrs ctxt = 
   150 fun equivariance pred_trms raw_induct intrs ctxt = 
   151 let
   151 let
       
   152   val is_already_eqvt = 
       
   153     filter (is_eqvt ctxt) pred_trms
       
   154     |> map (Syntax.string_of_term ctxt)
       
   155   val _ = if null is_already_eqvt then ()
       
   156     else error ("Already equivariant: " ^ commas is_already_eqvt)
       
   157 
   152   val pred_names = map (fst o dest_Const) pred_trms
   158   val pred_names = map (fst o dest_Const) pred_trms
   153   val raw_induct' = atomize_induct ctxt raw_induct
   159   val raw_induct' = atomize_induct ctxt raw_induct
   154   val intrs' = map atomize_intr intrs
   160   val intrs' = map atomize_intr intrs
   155   val (([raw_concl], [raw_pi]), ctxt') = 
   161   val (([raw_concl], [raw_pi]), ctxt') = 
   156     ctxt 
   162     ctxt