src/HOL/Tools/inductive_realizer.ML

     fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
       map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)),
             NoSyn);
-  in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
-    map constr_of_intr intrs)
+  in
+    ((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn),
+      map constr_of_intr intrs)
   end;
 
 fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
 
 (** turn "P" into "%r x. realizes r (P x)" **)

             (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
         end
       end) concls rec_names)
   end;
 
-fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
-  if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
+fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) =
+  if Binding.eq_name (name, s)
+  then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs))
   else x;
 
 fun add_dummies f [] _ thy =
       (([], NONE), thy)
   | add_dummies f dts used thy =